Nuprl Definition : dist
D(a;b;c;d;e;f) == ∃a',b',c':Point. ∃u:{u:Point| c' ≠ u} . (a'_b'_c' ∧ a'_u_c' ∧ ab ≅ a'b' ∧ cd ≅ b'c' ∧ ef ≅ a'u)
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,
set: {x:A| B[x]}
Definitions occuring in definition :
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
geo-point: Point,
geo-sep: a ≠ b,
geo-between: a_b_c,
and: P ∧ Q,
geo-congruent: ab ≅ cd
FDL editor aliases :
dist
Latex:
D(a;b;c;d;e;f) ==
\mexists{}a',b',c':Point. \mexists{}u:\{u:Point| c' \mneq{} u\} . (a'\_b'\_c' \mwedge{} a'\_u\_c' \mwedge{} ab \mcong{} a'b' \mwedge{} cd \mcong{} b'c' \mwedge{} ef \mcong{} a'u)
Date html generated:
2019_10_16-PM-02_43_53
Last ObjectModification:
2018_09_14-PM-08_37_38
Theory : euclidean!plane!geometry
Home
Index