Nuprl Lemma : sq_stable-geo-axioms-if
∀[g:GeometryPrimitives]
((∀a,b,c:Point. SqStable(B(abc)))
⇒ (∀a,b,c,d:Point. SqStable(ab ≅ cd))
⇒ (∀a,b,c,d:Point. SqStable(ab>cd))
⇒ (∀a,b,c:Point. (SqStable(a # bc) ∧ (BasicGeometryAxioms(g) ⇒ a leftof bc ⇒ (¬a leftof cb))))
⇒ SqStable(BasicGeometryAxioms(g)))
Proof
Definitions occuring in Statement :
basic-geo-axioms: BasicGeometryAxioms(g),
geo-congruent: ab ≅ cd,
geo-between: B(abc),
geo-lsep: a # bc,
geo-left: a leftof bc,
geo-gt-prim: ab>cd,
geo-primitives: GeometryPrimitives,
geo-point: Point,
sq_stable: SqStable(P),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
sq_stable: SqStable(P),
member: t ∈ T,
prop: ℙ,
all: ∀x:A. B[x],
and: P ∧ Q,
not: ¬A,
false: False,
squash: ↓T,
basic-geo-axioms: BasicGeometryAxioms(g),
geo-ge: ab ≥ cd,
so_lambda: λ2x.t[x],
so_apply: x[s],
geo-between: B(abc),
geo-congruent: ab ≅ cd,
guard: {T},
geo-sep: a # b,
geo-lsep: a # bc,
or: P ∨ Q
Latex:
\mforall{}[g:GeometryPrimitives]
((\mforall{}a,b,c:Point. SqStable(B(abc)))
{}\mRightarrow{} (\mforall{}a,b,c,d:Point. SqStable(ab \mcong{} cd))
{}\mRightarrow{} (\mforall{}a,b,c,d:Point. SqStable(ab>cd))
{}\mRightarrow{} (\mforall{}a,b,c:Point. (SqStable(a \# bc) \mwedge{} (BasicGeometryAxioms(g) {}\mRightarrow{} a leftof bc {}\mRightarrow{} (\mneg{}a leftof cb))))
{}\mRightarrow{} SqStable(BasicGeometryAxioms(g)))
Date html generated:
2020_05_20-AM-09_41_27
Last ObjectModification:
2020_03_14-AM-09_31_03
Theory : euclidean!plane!geometry
Home
Index