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: b supposing a
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
Definitions unfolded in proof : 
qge: a ≥ b
, 
true: True
, 
squash: ↓T
, 
cand: A c∧ B
, 
ifthenelse: if b then t else f fi 
, 
band: p ∧b q
, 
bfalse: ff
, 
guard: {T}
, 
sq_type: SQType(T)
, 
subtype_rel: A ⊆r B
, 
or: P ∨ Q
, 
rev_implies: P 
⇐ Q
, 
pi2: snd(t)
, 
pi1: fst(t)
, 
iff: P 
⇐⇒ 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: b supposing a
, 
implies: P 
⇒ 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