Nuprl Definition : geo-lt
p < q == ∃a,b:Point. (a ≠ b ∧ p + |ab| ≤ q)
Definitions occuring in Statement :
geo-add-length: p + q,
geo-le: p ≤ q,
geo-length: |s|,
geo-mk-seg: ab,
geo-sep: a ≠ b,
geo-point: Point,
exists: ∃x:A. B[x],
and: P ∧ Q
Definitions occuring in definition :
exists: ∃x:A. B[x],
geo-point: Point,
and: P ∧ Q,
geo-sep: a ≠ b,
geo-le: p ≤ q,
geo-add-length: p + q,
geo-length: |s|,
geo-mk-seg: ab
FDL editor aliases :
geo-lt
geo-lt
Latex:
p < q == \mexists{}a,b:Point. (a \mneq{} b \mwedge{} p + |ab| \mleq{} q)
Date html generated:
2017_10_02-PM-06_18_38
Last ObjectModification:
2017_08_05-PM-04_13_16
Theory : euclidean!plane!geometry
Home
Index