Nuprl Definition : real-interval-lattice
real-interval-lattice(I) == mk-distributive-lattice({r:ℝ| r ∈ I} ; λ2x y.rmin(x;y); λ2x y.rmax(x;y))
Definitions occuring in Statement :
mk-distributive-lattice: mk-distributive-lattice(T; m; j)
,
i-member: r ∈ I
,
rmin: rmin(x;y)
,
rmax: rmax(x;y)
,
real: ℝ
,
so_lambda: λ2x y.t[x; y]
,
set: {x:A| B[x]}
Definitions occuring in definition :
mk-distributive-lattice: mk-distributive-lattice(T; m; j)
,
set: {x:A| B[x]}
,
real: ℝ
,
i-member: r ∈ I
,
rmin: rmin(x;y)
,
so_lambda: λ2x y.t[x; y]
,
rmax: rmax(x;y)
FDL editor aliases :
real-interval-lattice
Latex:
real-interval-lattice(I) == mk-distributive-lattice(\{r:\mBbbR{}| r \mmember{} I\} ; \mlambda{}\msubtwo{}x y.rmin(x;y); \mlambda{}\msubtwo{}x y.rmax(x;y)\000C)
Date html generated:
2016_05_18-AM-11_50_26
Last ObjectModification:
2015_10_16-PM-03_25_39
Theory : lattices
Home
Index