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