Nuprl Definition : real-closed-interval-lattice

For real numbers ⌜a ≤ b⌝the reals in the closed interval ⌜[a, b]⌝
form distributive lattice with meet ⌜rmin(x;y)⌝ and join ⌜rmax(x;y)⌝.
But they do not form bounded distributive lattice with and 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 ⌜y⌝).

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

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

Definitions occuring in Statement :  rccint: [l, u] i-member: r ∈ I rmin: rmin(x;y) rmax: rmax(x;y) req: y real: so_lambda: λ2y.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

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