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:\Sigma, s:\mathbb{N} \to \Sigma \vdash i(s, x):\left(\prod_{n:\mathbb{N}}(s(n) \leq 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.