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