Showing changes from revision #3 to #4: Added | Removed | Changed

Contents

Definition

A $\sigma$-complete lattice is a lattice $(L, \leq, \bot, \vee, \top, \wedge)$ with

• a function

  $$\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to L) \to L$$

• a family of dependent terms

  $$n:\mathbb{N}, s:\mathbb{N} \to L \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n)$$

• a family of dependent terms

  $$x:\mathrm{<span><del\; class="diffmod">\; L</del><ins\; class="diffmod">\; \Sigma </ins></span>},n:\mathbb{N},s:\mathbb{N}\to \mathrm{<span><del\; class="diffmod">\; L</del><ins\; class="diffmod">\; \Sigma </ins></span>}⊢i(n,s,x):((\prod _{n:\mathbb{N}}(s(n)\le x))s(n)\le x)\to (\underset{n:\mathbb{N}}{\bigvee }s(n)\le x)$$ x:L, x:\Sigma, n:\mathbb{N}, s:\mathbb{N} \to L \Sigma \vdash i(n, i(s, s, x):\left(\prod_{n:\mathbb{N}}(s(n) x):(s(n) \leq x) x)\right) \to \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)

representing that denumerable/countable joins exist in the lattice.

See also

• lattice

• sigma-frame

• sigma-continuous valuation

• sigma-continuous probability valuation

• omega-complete poset

References

• Alex Simpson, Measure, randomness and sublocales.