Nuprl Definition : hp-angle-sum
abc + xyz ≅ def == ∃p,p',d',f':Point. (((abc ≅a dep ∧ fep ≅a xyz) ∧ e_p'_p) ∧ (out(e dd') ∧ out(e ff')) ∧ d'-p'-f')
Definitions occuring in Statement :
geo-out: out(p ab),
geo-cong-angle: abc ≅a xyz,
geo-strict-between: a-b-c,
geo-between: a_b_c,
geo-point: Point,
exists: ∃x:A. B[x],
and: P ∧ Q
Definitions occuring in definition :
exists: ∃x:A. B[x],
geo-point: Point,
geo-cong-angle: abc ≅a xyz,
geo-between: a_b_c,
and: P ∧ Q,
geo-out: out(p ab),
geo-strict-between: a-b-c
FDL editor aliases :
hp-angle-sum
Latex:
abc + xyz \mcong{} def ==
\mexists{}p,p',d',f':Point. (((abc \mcong{}\msuba{} dep \mwedge{} fep \mcong{}\msuba{} xyz) \mwedge{} e\_p'\_p) \mwedge{} (out(e dd') \mwedge{} out(e ff')) \mwedge{} d'-p'-f')
Date html generated:
2019_10_16-PM-02_02_40
Last ObjectModification:
2019_05_31-PM-02_31_57
Theory : euclidean!plane!geometry
Home
Index