Nuprl Lemma : compatible-same-dim-cubes-with-interior-point
∀[k:ℕ]. ∀[a,b:ℚCube(k)].
(a = b ∈ ℚCube(k)) supposing
((∃x:ℕk ⟶ ℚ. (rat-point-in-cube-interior(k;x;a) ∧ rat-point-in-cube(k;x;b))) and
Compatible(a;b) and
(dim(a) = dim(b) ∈ ℤ))
Proof
Definitions occuring in Statement :
compatible-rat-cubes: Compatible(c;d),
rat-cube-dimension: dim(c),
rat-point-in-cube-interior: rat-point-in-cube-interior(k;x;a),
rat-point-in-cube: rat-point-in-cube(k;x;c),
rational-cube: ℚCube(k),
rationals: ℚ,
int_seg: {i..j-},
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
uimplies: b supposing a,
exists: ∃x:A. B[x],
and: P ∧ Q,
uiff: uiff(P;Q),
prop: ℙ,
nat: ℕ,
subtype_rel: A ⊆r B,
int_seg: {i..j-},
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
compatible-cubes-with-interior-point,
rat-cube-face-dimension-equal,
inhabited-rat-cube-iff-point,
rat-point-in-cube_wf,
int_seg_wf,
rationals_wf,
rat-point-in-cube-interior_wf,
compatible-rat-cubes_wf,
istype-int,
rat-cube-dimension_wf,
set_subtype_base,
lelt_wf,
int_subtype_base
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_isectElimination,
isectElimination,
productElimination,
because_Cache,
dependent_pairFormation_alt,
universeIsType,
sqequalRule,
productIsType,
functionIsType,
natural_numberEquality,
setElimination,
rename,
isect_memberEquality_alt,
axiomEquality,
isectIsTypeImplies,
inhabitedIsType,
equalityIstype,
applyEquality,
intEquality,
lambdaEquality_alt,
minusEquality,
addEquality,
sqequalBase,
equalitySymmetry
Latex:
\mforall{}[k:\mBbbN{}]. \mforall{}[a,b:\mBbbQ{}Cube(k)].
(a = 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) and
(dim(a) = dim(b)))
Date html generated:
2020_05_20-AM-09_20_49
Last ObjectModification:
2019_11_14-PM-09_16_24
Theory : rationals
Home
Index