#Contents# * table of contents {:toc} ## 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](https://www.sciencedirect.com/science/article/pii/S0168007211001874).