Nuprl Lemma : geo-sas
∀e:BasicGeometry. ∀a,b,c,A,B,C:Point.
(bc ≅ BC) supposing (((ab ≅ AB ∧ ac ≅ AC) ∧ bac ≅a BAC) and (Triangle(a;b;c) ∧ Triangle(A;B;C)))
Proof
Definitions occuring in Statement :
geo-cong-angle: abc ≅a xyz,
geo-tri: Triangle(a;b;c),
basic-geometry: BasicGeometry,
geo-congruent: ab ≅ cd,
geo-point: Point,
uimplies: b supposing a,
all: ∀x:A. B[x],
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
and: P ∧ Q,
geo-cong-angle: abc ≅a xyz,
exists: ∃x:A. B[x],
geo-tri: Triangle(a;b;c),
geo-congruent: ab ≅ cd,
not: ¬A,
implies: P ⇒ Q,
false: False,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
guard: {T},
prop: ℙ,
basic-geometry: BasicGeometry,
uiff: uiff(P;Q)
Latex:
\mforall{}e:BasicGeometry. \mforall{}a,b,c,A,B,C:Point.
(bc \mcong{} BC) supposing (((ab \mcong{} AB \mwedge{} ac \mcong{} AC) \mwedge{} bac \mcong{}\msuba{} BAC) and (Triangle(a;b;c) \mwedge{} Triangle(A;B;C)))
Date html generated:
2020_05_20-AM-09_58_40
Last ObjectModification:
2019_12_26-PM-08_32_40
Theory : euclidean!plane!geometry
Home
Index