Nuprl Definition : real-closed-interval-lattice

For real numbers ⌜a ≤ b⌝, the reals in the closed interval ⌜[a, b]⌝
form a distributive lattice with meet ⌜rmin(x;y)⌝ and join ⌜rmax(x;y)⌝.
But they do not form a bounded distributive lattice with 0 = a and 1 = b
because we can't prove that ⌜rmin(a;x)⌝ is the same real as ⌜a⌝.
We can only prove that it is an "equivalent" real using the `req` relation
(that we display ⌜x = y⌝).

Thus the closed interval forms a generalized-bounded-distributive-lattice.⋅

real-closed-interval-lattice(a;b) ==  mk-general-bounded-dist-lattice({r:ℝ| r ∈ [a, b]} ;λ₂x y.rmin(x;y);λ₂x y.rmax(x;y)\000C;a;b;λ₂x y.x = y)

Definitions occuring in Statement : rccint: [l, u], i-member: r ∈ I, rmin: rmin(x;y), rmax: rmax(x;y), req: x = y, real: ℝ, so_lambda: λ₂x y.t[x; y], set: {x:A| B[x]} , mk-general-bounded-dist-lattice: mk-general-bounded-dist-lattice(T;m;j;z;o;E)
FDL editor aliases : real-closed-interval-lattice

Latex:
real-closed-interval-lattice(a;b) == mk-general-bounded-dist-lattice(\{r:\mBbbR{}| r \mmember{} [a, b]\} ;\mlambda{}\msubtwo{}x y.rmin(x;y);\mlambda{}\msubtwo{}x y.rmax(x;y);a;b;\mlambda{}\msubtwo{}x y.x = y\000C) Date html generated: 2020_05_20-AM-11_33_50 Last ObjectModification: 2020_01_16-PM-03_28_18 Theory : reals Home Index