Nuprl Lemma : faces-of-compatible-rat-cubes
∀k:ℕ. ∀f,g,c,d:ℚCube(k). ((↑Inhabited(c)) ⇒ (↑Inhabited(d)) ⇒ f ≤ c ⇒ g ≤ d ⇒ Compatible(c;d) ⇒ Compatible(f;g))
Proof
Definitions occuring in Statement :
compatible-rat-cubes: Compatible(c;d),
inhabited-rat-cube: Inhabited(c),
rat-cube-face: c ≤ d,
rational-cube: ℚCube(k),
nat: ℕ,
assert: ↑b,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
label: ...$L... t,
true: True,
squash: ↓T,
subtype_rel: A ⊆r B,
rev_implies: P ⇐ Q,
cand: A c∧ B,
iff: P ⇐⇒ Q,
pi1: fst(t),
pi2: snd(t),
top: Top,
so_apply: x[s],
so_lambda: λ2x.t[x],
or: P ∨ Q,
rat-point-interval: [a],
rat-interval-face: I ≤ J,
inhabited-rat-interval: Inhabited(I),
rat-interval-intersection: I ⋂ J,
rational-interval: ℚInterval,
rational-cube: ℚCube(k),
rat-cube-intersection: c ⋂ d,
rat-cube-face: c ≤ d,
guard: {T},
nat: ℕ,
rev_uimplies: rev_uimplies(P;Q),
uimplies: b supposing a,
and: P ∧ Q,
uiff: uiff(P;Q),
prop: ℙ,
member: t ∈ T,
uall: ∀[x:A]. B[x],
compatible-rat-cubes: Compatible(c;d),
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
top_wf,
subtype_rel_product,
istype-top,
istype-universe,
equal_wf,
qle_antisymmetry,
true_wf,
squash_wf,
assert_functionality_wrt_uiff,
rat-point-interval_wf,
rat-interval-intersection_wf,
compatible-rat-intervals-iff,
q_le_wf,
rat-interval-face_wf,
iff_weakening_equal,
assert-q_le-eq,
qmax_wf,
subtype_rel_self,
rational-interval_wf,
qle_weakening_eq_qorder,
qle_transitivity_qorder,
qmin_ub,
qle_wf,
iff_weakening_uiff,
qmin_wf,
qmax_lb,
istype-void,
pi1_wf_top,
rationals_wf,
pi2_wf,
int_seg_wf,
assert-inhabited-rat-cube,
istype-nat,
rational-cube_wf,
rat-cube-face_wf,
compatible-rat-cubes_wf,
rat-cube-intersection_wf,
inhabited-rat-cube_wf,
istype-assert
Rules used in proof :
universeEquality,
instantiate,
dependent_set_memberEquality_alt,
inlFormation_alt,
inrFormation_alt,
baseClosed,
imageMemberEquality,
imageElimination,
spreadEquality,
productIsType,
equalityIstype,
unionIsType,
promote_hyp,
independent_pairFormation,
independent_functionElimination,
productEquality,
because_Cache,
equalitySymmetry,
equalityTransitivity,
voidElimination,
isect_memberEquality_alt,
independent_pairEquality,
lambdaEquality_alt,
applyLambdaEquality,
unionElimination,
applyEquality,
sqequalRule,
rename,
setElimination,
natural_numberEquality,
dependent_functionElimination,
independent_isectElimination,
productElimination,
inhabitedIsType,
universeIsType,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
extract_by_obid,
introduction,
cut,
sqequalHypSubstitution,
lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}k:\mBbbN{}. \mforall{}f,g,c,d:\mBbbQ{}Cube(k).
((\muparrow{}Inhabited(c)) {}\mRightarrow{} (\muparrow{}Inhabited(d)) {}\mRightarrow{} f \mleq{} c {}\mRightarrow{} g \mleq{} d {}\mRightarrow{} Compatible(c;d) {}\mRightarrow{} Compatible(f;g))
Date html generated:
2019_10_29-AM-07_54_31
Last ObjectModification:
2019_10_19-AM-02_12_10
Theory : rationals
Home
Index