Nuprl Definition : qrle
qrle(x;y) == ↓∃a,b:ℝ. ((a = x ∈ [ℝ]) ∧ (b = y ∈ [ℝ]) ∧ (a ≤ b))
Definitions occuring in Statement :
qreal: [ℝ],
rleq: x ≤ y,
real: ℝ,
exists: ∃x:A. B[x],
squash: ↓T,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
rleq: x ≤ y,
qreal: [ℝ],
equal: s = t ∈ T,
and: P ∧ Q,
real: ℝ,
exists: ∃x:A. B[x],
squash: ↓T
FDL editor aliases :
qrle
Latex:
qrle(x;y) == \mdownarrow{}\mexists{}a,b:\mBbbR{}. ((a = x) \mwedge{} (b = y) \mwedge{} (a \mleq{} b))
Date html generated:
2016_10_26-PM-00_51_21
Last ObjectModification:
2016_09_12-PM-05_47_48
Theory : reals_2
Home
Index