Nuprl Lemma : geo-congruent-implies-ge
∀[g:BasicGeometry-]. ∀[c,d,a,b:Point]. cd ≥ ab supposing cd ≅ ab
Proof
Definitions occuring in Statement :
basic-geometry-: BasicGeometry-,
geo-ge: ab ≥ cd,
geo-congruent: ab ≅ cd,
geo-point: Point,
uimplies: b supposing a,
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
guard: {T},
false: False,
prop: ℙ,
subtype_rel: A ⊆r B,
or: P ∨ Q,
geo-length-sep: ab # cd),
geo-congruent: ab ≅ cd,
implies: P ⇒ Q,
not: ¬A,
geo-ge: ab ≥ cd,
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Latex:
\mforall{}[g:BasicGeometry-]. \mforall{}[c,d,a,b:Point]. cd \mgeq{} ab supposing cd \mcong{} ab
Date html generated:
2020_05_20-AM-09_48_50
Last ObjectModification:
2019_12_20-PM-07_38_05
Theory : euclidean!plane!geometry
Home
Index