Nuprl Lemma : in-rat-cube-face

[k:ℕ]. ∀[p:ℝ^k]. ∀[c,f:ℚCube(k)].  (in-rat-cube(k;p;c)) supposing (in-rat-cube(k;p;f) and (↑Inhabited(c)) and f ≤ c)


Proof




Definitions occuring in Statement :  in-rat-cube: in-rat-cube(k;p;c) real-vec: ^n nat: assert: b uimplies: supposing a uall: [x:A]. B[x] inhabited-rat-cube: Inhabited(c) rat-cube-face: c ≤ d rational-cube: Cube(k)
Definitions unfolded in proof :  rge: x ≥ y rev_uimplies: rev_uimplies(P;Q) le: A ≤ B rnonneg: rnonneg(x) rleq: x ≤ y nat: subtype_rel: A ⊆B iff: ⇐⇒ Q guard: {T} cand: c∧ B inhabited-rat-interval: Inhabited(I) prop: top: Top so_apply: x[s] so_lambda: λ2x.t[x] or: P ∨ Q rat-point-interval: [a] pi2: snd(t) pi1: fst(t) rat-interval-face: I ≤ J rational-interval: Interval rational-cube: Cube(k) implies:  Q real-vec: ^n rat-cube-face: c ≤ d all: x:A. B[x] in-rat-cube: in-rat-cube(k;p;c) and: P ∧ Q uiff: uiff(P;Q) uimplies: supposing a member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  rleq_weakening_equal rleq_functionality_wrt_implies rleq-rat2real istype-nat real-vec_wf rational-cube_wf rat-cube-face_wf inhabited-rat-cube_wf in-rat-cube_wf le_witness_for_triv int_seg_wf subtype_rel_self rational-interval_wf q_le_wf istype-assert iff_weakening_equal assert-q_le-eq qle_wf rat2real_wf rleq_wf istype-void pi1_wf_top rationals_wf pi2_wf assert-inhabited-rat-cube
Rules used in proof :  isectIsTypeImplies functionIsTypeImplies rename setElimination natural_numberEquality equalityIstype unionIsType productIsType because_Cache equalityTransitivity independent_functionElimination universeIsType independent_pairFormation productEquality hyp_replacement equalitySymmetry promote_hyp voidElimination isect_memberEquality_alt independent_pairEquality lambdaEquality_alt applyLambdaEquality unionElimination sqequalRule inhabitedIsType applyEquality dependent_functionElimination lambdaFormation_alt independent_isectElimination productElimination hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[p:\mBbbR{}\^{}k].  \mforall{}[c,f:\mBbbQ{}Cube(k)].
    (in-rat-cube(k;p;c))  supposing  (in-rat-cube(k;p;f)  and  (\muparrow{}Inhabited(c))  and  f  \mleq{}  c)



Date html generated: 2019_10_30-AM-10_12_51
Last ObjectModification: 2019_10_27-AM-00_17_24

Theory : real!vectors


Home Index