#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In set theory ### In measure theory, a __measure__ on a [[sigma-frame|$\sigma$-frame]] or more generally a [[sigma-complete lattice|$\sigma$-complete]] [[distributive lattice]] $(L, \leq, \bot, \vee, \top, \wedge, \Vee)$ is a [[valuation (measure theory)|valuation]] $\mu:L \to [0, \infty]$ such that the elements are mutually disjoint and the probability valuation is denumerably/countably additive $$\forall s\in L^\mathbb{N}. \forall m \in \mathbb{N}. \forall n \in \mathbb{N}. (m \neq n) \wedge (s(m) \wedge s(n) = \bot)$$ $$\forall s\in L^\mathbb{N}. \mu(\Vee_{n:\mathbb{N}} s(n)) = \sum_{n:\mathbb{N}} \mu(s(n))$$ ### In homotopy type theory ### In measure theory, a __measure__ on a [[sigma-frame|$\sigma$-frame]] or more generally a [[sigma-complete lattice |$\sigma$-complete]] [[distributive lattice]] $(L, \leq, \bot, \vee, \top, \wedge, \Vee)$ is a [[valuation (measure theory)|valuation]] $\mu:L \to [0, \infty]$ with * a family of dependent terms $$s:\mathbb{N} \to L \vdash \alpha(s):\left(\prod_{m:\mathbb{N}} \prod_{n:\mathbb{N}} (m \neq n) \times (s(m) \wedge s(n) = \bot)\right) \times \left(\mu(\Vee_{n:\mathbb{N}} s(n)) = \sum_{n:\mathbb{N}} \mu(s(n)) \right)$$ representing the mutually disjoint elements condition and the denumerably/countably additive condition. ## See also ## * [[sigma-frame]] * [[sigma-complete lattice]] * [[distributive lattice]] * [[valuation (measure theory)]] * [[sigma-continuous valuation]] * [[probability measure]] ## References ## * Alex Simpson, [Measure, randomness and sublocales](https://www.sciencedirect.com/science/article/pii/S0168007211001874).