Nuprl Definition : tar-cong-angle
TAabc=TAxyz ==
a ≠ b
∧ c ≠ b
∧ x ≠ y
∧ z ≠ y
∧ (∃a',c',x',z':Point
(((b_a_a' ∧ b_c_c' ∧ y_x_x' ∧ y_z_z' ∧ aa' ≅ yx ∧ cc' ≅ yz ∧ a'c' ≅ x'z') ∧ xx' ≅ ba) ∧ zz' ≅ bc))
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 :
tar-cong-angle
tar-cong-angle
tar-cong-angle
Latex:
TAabc=TAxyz ==
a \mneq{} b
\mwedge{} c \mneq{} b
\mwedge{} x \mneq{} y
\mwedge{} z \mneq{} y
\mwedge{} (\mexists{}a',c',x',z':Point
(((b\_a\_a' \mwedge{} b\_c\_c' \mwedge{} y\_x\_x' \mwedge{} y\_z\_z' \mwedge{} aa' \00D0 yx \mwedge{} cc' \00D0 yz \mwedge{} a'c' \00D0 x'z') \mwedge{} xx' \00D0 ba)
\mwedge{} zz' \00D0 bc))
Date html generated:
2017_10_02-PM-06_23_45
Last ObjectModification:
2017_08_05-PM-04_17_55
Theory : euclidean!plane!geometry
Home
Index