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 :
squash: ↓T,
exists: ∃x:A. B[x],
real: ℝ,
and: P ∧ Q,
equal: s = t ∈ T,
qreal: [ℝ],
rleq: x ≤ y
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_05_18-AM-11_15_12
Last ObjectModification:
2015_10_18-PM-08_32_21
Theory : reals
Home
Index