Nuprl Lemma : inhabited-iff-in-rat-cube

[k:ℕ]. ∀c:ℚCube(k). (↑Inhabited(c) ⇐⇒ ∃p:ℝ^k. in-rat-cube(k;p;c))


Proof




Definitions occuring in Statement :  in-rat-cube: in-rat-cube(k;p;c) real-vec: ^n nat: assert: b uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q inhabited-rat-cube: Inhabited(c) rational-cube: Cube(k)
Definitions unfolded in proof :  guard: {T} le: A ≤ B rnonneg: rnonneg(x) rleq: x ≤ y cand: c∧ B pi2: snd(t) inhabited-rat-interval: Inhabited(I) in-rat-cube: in-rat-cube(k;p;c) nat: pi1: fst(t) rational-interval: Interval rational-cube: Cube(k) real-vec: ^n prop: exists: x:A. B[x] rev_uimplies: rev_uimplies(P;Q) rev_implies:  Q uimplies: supposing a uiff: uiff(P;Q) member: t ∈ T implies:  Q and: P ∧ Q iff: ⇐⇒ Q all: x:A. B[x] uall: [x:A]. B[x]
Lemmas referenced :  rleq_wf rleq_transitivity q_le_wf iff_weakening_equal assert-q_le-eq qle_wf le_witness_for_triv rleq-rat2real rleq_weakening_equal int_seg_wf rat2real_wf istype-nat rational-cube_wf in-rat-cube_wf real-vec_wf assert_witness inhabited-rat-cube_wf istype-assert assert-inhabited-rat-cube
Rules used in proof :  functionIsTypeImplies independent_pairEquality rename setElimination natural_numberEquality dependent_functionElimination equalitySymmetry equalityTransitivity equalityIstype inhabitedIsType applyEquality lambdaEquality_alt dependent_pairFormation_alt universeIsType productIsType sqequalRule independent_functionElimination because_Cache independent_isectElimination productElimination hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut independent_pairFormation lambdaFormation_alt isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}c:\mBbbQ{}Cube(k).  (\muparrow{}Inhabited(c)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}p:\mBbbR{}\^{}k.  in-rat-cube(k;p;c))



Date html generated: 2019_10_30-AM-10_13_02
Last ObjectModification: 2019_10_29-PM-01_49_09

Theory : real!vectors


Home Index