Nuprl Lemma : in-rat-cube-intersection

k:ℕ. ∀c,d:ℚCube(k). ∀x:ℝ^k.  (in-rat-cube(k;x;c ⋂ d) ⇐⇒ in-rat-cube(k;x;c) ∧ in-rat-cube(k;x;d))


Proof




Definitions occuring in Statement :  in-rat-cube: in-rat-cube(k;p;c) real-vec: ^n nat: all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q rat-cube-intersection: c ⋂ d rational-cube: Cube(k)
Definitions unfolded in proof :  rge: x ≥ y rev_uimplies: rev_uimplies(P;Q) guard: {T} or: P ∨ Q uimplies: supposing a uiff: uiff(P;Q) rev_implies:  Q nat: prop: uall: [x:A]. B[x] cand: c∧ B pi2: snd(t) pi1: fst(t) rat-interval-intersection: I ⋂ J rational-interval: Interval real-vec: ^n rational-cube: Cube(k) rat-cube-intersection: c ⋂ d member: t ∈ T in-rat-cube: in-rat-cube(k;p;c) implies:  Q and: P ∧ Q iff: ⇐⇒ Q all: x:A. B[x]
Lemmas referenced :  rat2real-qmin rmin_ub rmin_wf req_weakening rat2real-qmax rleq_functionality rmax_lb rmax_wf qmin_lb qmax_ub rleq_weakening_equal rleq_functionality_wrt_implies qle_wf qle_reflexivity rleq-rat2real istype-nat rational-cube_wf real-vec_wf rat-cube-intersection_wf in-rat-cube_wf int_seg_wf qmin_wf qmax_wf rat2real_wf rleq_wf
Rules used in proof :  inrFormation_alt inlFormation_alt independent_isectElimination because_Cache rename setElimination natural_numberEquality independent_functionElimination equalitySymmetry equalityTransitivity equalityIstype isectElimination extract_by_obid introduction universeIsType productIsType productElimination inhabitedIsType applyEquality sqequalRule hypothesisEquality thin dependent_functionElimination hypothesis cut sqequalHypSubstitution independent_pairFormation lambdaFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}c,d:\mBbbQ{}Cube(k).  \mforall{}x:\mBbbR{}\^{}k.    (in-rat-cube(k;x;c  \mcap{}  d)  \mLeftarrow{}{}\mRightarrow{}  in-rat-cube(k;x;c)  \mwedge{}  in-rat-cube(k;x;d))



Date html generated: 2019_11_04-PM-04_43_06
Last ObjectModification: 2019_11_04-PM-03_55_44

Theory : real!vectors


Home Index