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 :
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]} ,
mk-distributive-lattice: mk-distributive-lattice(T; m; j)
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:
2020_05_20-AM-11_34_25
Last ObjectModification:
2020_01_16-PM-03_29_08
Theory : reals
Home
Index