▾ Set of symbols
▾ Alphabet
▾ Deduction system
▾ Theory
▾ Zermelo-Fraenkel set theory
▾ Set
▾ Subset
▾ Power set
▾ Hyperpower set sequence
▾ Hyperpower set
▾ Hypersubset
▾ Subset algebra
▾ Subset structure
▾ Measurable space
Measure space
Formulation 0
A D5107: Triple $M = (X, \mathcal{F}, \mu)$ is a measure space if and only if
(1) $(X, \mathcal{F})$ is a D1108: Measurable space
(2) $\mu$ is an D85: Unsigned basic measure on $(X, \mathcal{F})$
Subdefinitions
» D1159: Probability space
Child definitions
» D4248: Almost everywhere constant map
» D2940: Measure-preserving endomorphism
» D1732: Pushforward measure
Results
» R4453: Probability of symmetric difference of event and subevent
» R3645: Countable partition additivity of unsigned basic measure
» R975: Isotonicity of unsigned basic measure
» R3971: Intersection of sets of infinite measure need not have infinite measure
» R3969: Measure of intersection finite if measure of at least one set finite
» R982: Sequential continuity of measure from below
» R983: Sequential continuity of measure from above
» R3970: Measure of finite union finite iff measure of all sets in union finite
» R979: Countable subadditivity of measure
» R4277: Measure of measurable set complement
» R976: Finite disjoint additivity of unsigned basic measure
» R2086: Finite inclusion-exclusion principle for unsigned basic measure
» R4317: Inclusion-exclusion principle for unsigned basic measure of ternary union
» R4318: Inclusion-exclusion principle for unsigned basic measure of binary union
» R978: Measure of set difference
» R4443: Measure of symmetric difference of set and subset
» R4445: Inclusion-exclusion principle for probability of binary union
» R1234: Borel-Cantelli lemma
» R4502: Difference of almost everywhere equal euclidean complex functions is almost everywhere zero
» R4773: Inclusion-exclusion lower bound to probability of ternary intersection
» R4774:
» R4770: Inclusion-exclusion lower bound to probability of binary intersection
» R4769:
» R4841: Finite disjoint additivity of probability measure
» R4926: Finite partition additivity of unsigned basic measure
» R4927: Binary partition additivity of unsigned basic measure