Nuprl Lemma : in-rat-cube_wf

[k:ℕ]. ∀[p:ℝ^k]. ∀[c:ℚCube(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: uall: [x:A]. B[x] prop: member: t ∈ T rational-cube: Cube(k)
Definitions unfolded in proof :  pi2: snd(t) real-vec: ^n pi1: fst(t) rational-interval: Interval implies:  Q rational-cube: Cube(k) and: P ∧ Q nat: all: x:A. B[x] prop: in-rat-cube: in-rat-cube(k;p;c) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  istype-nat real-vec_wf rational-cube_wf rat2real_wf rleq_wf int_seg_wf
Rules used in proof :  isectIsTypeImplies isect_memberEquality_alt universeIsType axiomEquality because_Cache independent_functionElimination dependent_functionElimination equalitySymmetry equalityTransitivity equalityIstype productElimination lambdaFormation_alt inhabitedIsType applyEquality productEquality hypothesis hypothesisEquality rename setElimination natural_numberEquality thin isectElimination sqequalHypSubstitution extract_by_obid functionEquality sqequalRule cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[p:\mBbbR{}\^{}k].  \mforall{}[c:\mBbbQ{}Cube(k)].    (in-rat-cube(k;p;c)  \mmember{}  \mBbbP{})



Date html generated: 2019_10_30-AM-10_12_46
Last ObjectModification: 2019_10_26-AM-11_50_27

Theory : real!vectors


Home Index