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 :
mk-general-bounded-dist-lattice: mk-general-bounded-dist-lattice(T;m;j;z;o;E),
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]}
Definitions occuring in definition :
mk-general-bounded-dist-lattice: mk-general-bounded-dist-lattice(T;m;j;z;o;E),
set: {x:A| B[x]} ,
real: ℝ,
i-member: r ∈ I,
rccint: [l, u],
rmin: rmin(x;y),
rmax: rmax(x;y),
so_lambda: λ2x y.t[x; y],
req: x = y
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:
2016_07_08-PM-06_30_39
Last ObjectModification:
2016_01_13-PM-04_35_33
Theory : lattices
Home
Index