ThmDex – An index of mathematical definitions, results, and conjectures.
 ▼ Set of symbols ▼ Alphabet ▼ Deduction system ▼ Theory ▼ Zermelo-Fraenkel set theory ▼ Set ▼ Binary cartesian set product ▼ Binary relation ▼ Map ▼ Function ▼ Measure ▼ Real measure ▼ Euclidean real measure ▼ Complex measure ▼ Basic measure ▼ Unsigned basic measure
Definition D1734
Outer measure

Let $X$ be a D11: Set.
A D992: Function $\upsilon : \mathcal{P}(X) \to [0, \infty]$ is an outer measure on $X$ if and only if
 Condition Comment (1) $$\upsilon(\emptyset) = 0$$ Preserves order-zero from $(\mathcal{P}(X), \subseteq)$ to $([0, \infty], {\leq})$ (2) $$\forall \, E, F \in \mathcal{P}(X) \left( E \subseteq F \quad \implies \quad \upsilon(E) \leq \upsilon(F) \right)$$ ("D5371: Standard-isotone basic function") (3) $$\forall \, E_0, E_1, E_2, \dots \in \mathcal{P}(X) : \upsilon \left( \bigcup_{n \in \mathbb{N}} E_n \right) \leq \sum_{n \in \mathbb{N}} \upsilon(E_n)$$ Countably subadditive function from $(\mathcal{P}(X), \cup, \cap)$ to $([0, \infty], +, \times)$
Children
 ▶ Stieltjes outer measure