Nuprl Definition : circle-circumscription
circle-circumscription(e) == ∀a,b,c:Point. (b # ac ⇒ (∃m:Point. (am ≅ bm ∧ bm ≅ cm)))
Definitions occuring in Statement :
geo-lsep: a # bc,
geo-congruent: ab ≅ cd,
geo-point: Point,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
geo-lsep: a # bc,
exists: ∃x:A. B[x],
geo-point: Point,
and: P ∧ Q,
geo-congruent: ab ≅ cd
FDL editor aliases :
circle-circumscription
circle-circumscription
circle-circumscription
Latex:
circle-circumscription(e) == \mforall{}a,b,c:Point. (b \# ac {}\mRightarrow{} (\mexists{}m:Point. (am \00D0 bm \mwedge{} bm \00D0 cm)))
Date html generated:
2017_10_02-PM-06_53_57
Last ObjectModification:
2017_08_06-PM-07_48_01
Theory : euclidean!plane!geometry
Home
Index