Nuprl Lemma : compatible-cubes-with-interior-point
∀k:ℕ. ∀a,b:ℚCube(k).
(a ≤ b) supposing ((∃x:ℕk ⟶ ℚ. (rat-point-in-cube-interior(k;x;a) ∧ rat-point-in-cube(k;x;b))) and Compatible(a;b))
Proof
Definitions occuring in Statement :
compatible-rat-cubes: Compatible(c;d),
rat-point-in-cube-interior: rat-point-in-cube-interior(k;x;a),
rat-point-in-cube: rat-point-in-cube(k;x;c),
rat-cube-face: c ≤ d,
rational-cube: ℚCube(k),
rationals: ℚ,
int_seg: {i..j-},
nat: ℕ,
uimplies: b supposing a,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
function: x:A ⟶ B[x],
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
sq_stable: SqStable(P),
exists: ∃x:A. B[x],
and: P ∧ Q,
rat-point-in-cube: rat-point-in-cube(k;x;c),
rat-point-in-cube-interior: rat-point-in-cube-interior(k;x;a),
compatible-rat-cubes: Compatible(c;d),
uiff: uiff(P;Q),
cand: A c∧ B,
prop: ℙ,
squash: ↓T,
nat: ℕ,
true: True,
subtype_rel: A ⊆r B,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
sq_stable_from_decidable,
rat-cube-face_wf,
decidable__rat-cube-face-ext,
inhabited-rat-cube-iff-point,
rat-cube-intersection_wf,
rat-point-in-intersection,
rat-point-in-cube_wf,
int_seg_wf,
rationals_wf,
rat-point-in-cube-interior_wf,
compatible-rat-cubes_wf,
rational-cube_wf,
istype-nat,
rat-point-in-cube-interior-not-in-face,
squash_wf,
true_wf,
subtype_rel_self,
iff_weakening_equal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
independent_functionElimination,
dependent_functionElimination,
productElimination,
because_Cache,
independent_isectElimination,
dependent_pairFormation_alt,
independent_pairFormation,
universeIsType,
sqequalRule,
imageMemberEquality,
baseClosed,
imageElimination,
productIsType,
functionIsType,
natural_numberEquality,
setElimination,
rename,
inhabitedIsType,
applyEquality,
lambdaEquality_alt,
equalityTransitivity,
equalitySymmetry,
instantiate,
universeEquality
Latex:
\mforall{}k:\mBbbN{}. \mforall{}a,b:\mBbbQ{}Cube(k).
(a \mleq{} b) supposing
((\mexists{}x:\mBbbN{}k {}\mrightarrow{} \mBbbQ{}. (rat-point-in-cube-interior(k;x;a) \mwedge{} rat-point-in-cube(k;x;b))) and
Compatible(a;b))
Date html generated:
2020_05_20-AM-09_20_43
Last ObjectModification:
2019_11_14-PM-09_09_47
Theory : rationals
Home
Index