Nuprl Definition : geo-cong-angle
abc ≅a xyz ==
(((a ≠ b ∧ b ≠ c) ∧ x ≠ y) ∧ y ≠ z)
∧ (∃a',c',x',z':Point. (b_a_a' ∧ b_c_c' ∧ y_x_x' ∧ y_z_z' ∧ ba' ≅ yx' ∧ bc' ≅ yz' ∧ a'c' ≅ x'z'))
Definitions occuring in Statement :
geo-congruent: ab ≅ cd,
geo-between: a_b_c,
geo-sep: a ≠ b,
geo-point: Point,
exists: ∃x:A. B[x],
and: P ∧ Q
Definitions occuring in definition :
geo-sep: a ≠ b,
exists: ∃x:A. B[x],
geo-point: Point,
geo-between: a_b_c,
and: P ∧ Q,
geo-congruent: ab ≅ cd
FDL editor aliases :
geo-conga
geo-conga
Latex:
abc \mcong{}\msuba{} xyz ==
(((a \mneq{} b \mwedge{} b \mneq{} c) \mwedge{} x \mneq{} y) \mwedge{} y \mneq{} z)
\mwedge{} (\mexists{}a',c',x',z':Point. (b\_a\_a' \mwedge{} b\_c\_c' \mwedge{} y\_x\_x' \mwedge{} y\_z\_z' \mwedge{} ba' \mcong{} yx' \mwedge{} bc' \mcong{} yz' \mwedge{} a'c' \mcong{} x'z'))
Date html generated:
2019_10_16-PM-01_21_54
Last ObjectModification:
2018_11_07-AM-09_57_18
Theory : euclidean!plane!geometry
Home
Index