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
Formulation 0
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) \begin{equation} \upsilon(\emptyset) = 0 \end{equation} Preserves order-zero from $(\mathcal{P}(X), \subseteq)$ to $([0, \infty], {\leq})$
(2) \begin{equation} \forall \, E, F \in \mathcal{P}(X) \left( E \subseteq F \quad \implies \quad \upsilon(E) \leq \upsilon(F) \right) \end{equation} ("D5371: Standard-isotone basic function")
(3) \begin{equation} \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) \end{equation} Countably subadditive function from $(\mathcal{P}(X), \cup, \cap)$ to $([0, \infty], +, \times)$
Children
Stieltjes outer measure