Nuprl Definition : angle-sum
abc + def ≅a xyz == ∃p:Point. ((p leftof xy ∧ p leftof yz) ∧ abc ≅a xyp ∧ def ≅a zyp)
Definitions occuring in Statement :
geo-cong-angle: abc ≅a xyz,
geo-left: a leftof bc,
geo-point: Point,
exists: ∃x:A. B[x],
and: P ∧ Q
Definitions occuring in definition :
exists: ∃x:A. B[x],
geo-point: Point,
geo-left: a leftof bc,
and: P ∧ Q,
geo-cong-angle: abc ≅a xyz
FDL editor aliases :
angle-sum
Latex:
abc + def \mcong{}\msuba{} xyz == \mexists{}p:Point. ((p leftof xy \mwedge{} p leftof yz) \mwedge{} abc \mcong{}\msuba{} xyp \mwedge{} def \mcong{}\msuba{} zyp)
Date html generated:
2019_10_16-PM-02_03_08
Last ObjectModification:
2019_06_10-PM-07_44_09
Theory : euclidean!plane!geometry
Home
Index