### 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]} ;λ2x y.rmin(x;y);λ2x y.rmax(x;y)\000C;a;b;λ2x 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: `λ2x 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