Nuprl Definition : geo-le
p ≤ q == ↓∃p',q':{p:Point| O_X_p} . ((p' = p ∈ Length) ∧ (q' = q ∈ Length) ∧ X_p'_q')
Definitions occuring in Statement :
geo-length-type: Length
,
geo-X: X
,
geo-O: O
,
geo-between: a_b_c
,
geo-point: Point
,
exists: ∃x:A. B[x]
,
squash: ↓T
,
and: P ∧ Q
,
set: {x:A| B[x]}
,
equal: s = t ∈ T
Definitions occuring in definition :
geo-X: X
,
geo-between: a_b_c
,
geo-length-type: Length
,
equal: s = t ∈ T
,
and: P ∧ Q
,
geo-O: O
,
geo-point: Point
,
set: {x:A| B[x]}
,
exists: ∃x:A. B[x]
,
squash: ↓T
FDL editor aliases :
geo-le
geo-le
Latex:
p \mleq{} q == \mdownarrow{}\mexists{}p',q':\{p:Point| O\_X\_p\} . ((p' = p) \mwedge{} (q' = q) \mwedge{} X\_p'\_q')
Date html generated:
2017_10_02-PM-04_51_54
Last ObjectModification:
2017_08_17-PM-01_30_48
Theory : euclidean!plane!geometry
Home
Index