Nuprl Definition : eu-cong-angle
abc = xyz ==
(¬(a = b ∈ Point))
∧ (¬(c = b ∈ Point))
∧ (¬(x = y ∈ Point))
∧ (¬(z = y ∈ Point))
∧ (∃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 :
eu-between-eq: a_b_c
,
eu-congruent: ab=cd
,
eu-point: Point
,
exists: ∃x:A. B[x]
,
not: ¬A
,
and: P ∧ Q
,
equal: s = t ∈ T
Definitions occuring in definition :
not: ¬A
,
equal: s = t ∈ T
,
exists: ∃x:A. B[x]
,
eu-point: Point
,
eu-between-eq: a_b_c
,
and: P ∧ Q
,
eu-congruent: ab=cd
FDL editor aliases :
eu-conga
Latex:
abc = xyz ==
(\mneg{}(a = b))
\mwedge{} (\mneg{}(c = b))
\mwedge{} (\mneg{}(x = y))
\mwedge{} (\mneg{}(z = y))
\mwedge{} (\mexists{}a',c',x',z':Point. (b\_a\_a' \mwedge{} b\_c\_c' \mwedge{} y\_x\_x' \mwedge{} y\_z\_z' \mwedge{} ba'=yx' \mwedge{} bc'=yz' \mwedge{} a'c'=x'z'))
Date html generated:
2016_06_16-PM-01_31_55
Last ObjectModification:
2016_05_20-PM-02_09_20
Theory : euclidean!geometry
Home
Index