Nuprl Lemma : half-cube-of-face

k:ℕ. ∀a,b,c,d,e:ℚCube(k).
  (Compatible(a;e)
   b ≤ e
   d ≤ c
   (b ≤ a) supposing ((↑Inhabited(e)) and (↑Inhabited(a)) and (↑is-half-cube(k;c;a)) and (↑is-half-cube(k;d;b))))


Proof




Definitions occuring in Statement :  compatible-rat-cubes: Compatible(c;d) inhabited-rat-cube: Inhabited(c) is-half-cube: is-half-cube(k;h;c) rat-cube-face: c ≤ d rational-cube: Cube(k) nat: assert: b uimplies: supposing a all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  qge: a ≥ b true: True squash: T cand: c∧ B ifthenelse: if then else fi  band: p ∧b q bfalse: ff guard: {T} sq_type: SQType(T) subtype_rel: A ⊆B or: P ∨ Q rev_implies:  Q pi2: snd(t) pi1: fst(t) iff: ⇐⇒ Q nat: rat-point-interval: [a] rat-interval-intersection: I ⋂ J rat-interval-face: I ≤ J is-half-interval: is-half-interval(I;J) inhabited-rat-interval: Inhabited(I) rational-interval: Interval rational-cube: Cube(k) rat-cube-intersection: c ⋂ d rat-cube-face: c ≤ d rev_uimplies: rev_uimplies(P;Q) and: P ∧ Q uiff: uiff(P;Q) prop: compatible-rat-cubes: Compatible(c;d) uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a implies:  Q all: x:A. B[x]
Lemmas referenced :  uiff_transitivity3 uiff_transitivity qle_connex qmin-eq-iff-1 qmax-eq-iff-1 qmin-eq-iff-2 qmax-eq-iff-2 qle-qavg-iff-4 qle_antisymmetry qavg-eq-iff-4 qavg-qle-iff-2 qmax-eq-iff qmin-eq-iff qavg-eq-iff-2 qle_functionality_wrt_implies qavg-eq-iff-8 qavg-eq-iff-3 qle_weakening_eq_qorder qle-qavg-iff-2 qle-qavg-iff-1 qavg-qle-iff-1 qavg-eq-iff-7 qavg-eq-iff-1 qle_transitivity_qorder qle_reflexivity member_wf qavg-same istype-universe true_wf squash_wf qmin_ub qmax_lb iff_weakening_equal assert-q_le-eq assert_of_band assert_of_bor iff_weakening_uiff iff_transitivity subtype_rel_self q_le_wf qmin_wf qmax_wf rationals_wf equal_wf bfalse_wf assert-qeq btrue_wf band_wf eqtt_to_assert bool_subtype_base bool_wf subtype_base_sq bool_cases qeq_wf2 bor_wf assert_wf rational-interval_wf qavg_wf qle_wf int_seg_wf rat-cube-intersection_wf assert-is-half-cube assert-inhabited-rat-cube istype-nat rational-cube_wf compatible-rat-cubes_wf rat-cube-face_wf istype-assert inhabited-rat-cube_wf is-half-cube_wf assert_witness
Rules used in proof :  functionIsType functionEquality baseClosed imageMemberEquality universeEquality imageElimination lambdaEquality_alt hyp_replacement inrFormation_alt promote_hyp inlFormation_alt isect_memberEquality_alt productEquality unionEquality cumulativity instantiate unionElimination unionIsType independent_pairEquality because_Cache applyLambdaEquality productIsType dependent_set_memberEquality_alt independent_pairFormation setElimination natural_numberEquality equalitySymmetry equalityTransitivity equalityIstype applyEquality dependent_functionElimination sqequalRule independent_isectElimination productElimination inhabitedIsType universeIsType rename independent_functionElimination hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut isect_memberFormation_alt lambdaFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}a,b,c,d,e:\mBbbQ{}Cube(k).
    (Compatible(a;e)
    {}\mRightarrow{}  b  \mleq{}  e
    {}\mRightarrow{}  d  \mleq{}  c
    {}\mRightarrow{}  (b  \mleq{}  a)  supposing 
                ((\muparrow{}Inhabited(e))  and 
                (\muparrow{}Inhabited(a))  and 
                (\muparrow{}is-half-cube(k;c;a))  and 
                (\muparrow{}is-half-cube(k;d;b))))



Date html generated: 2019_10_29-AM-07_55_14
Last ObjectModification: 2019_10_24-PM-05_39_25

Theory : rationals


Home Index