def IsLebesgueMeasureAxioms (n : ℕ) (M : Set (Set (Fin n → ℝ))) (m : Set (Fin n → ℝ) → ENNReal) : Prop

Definition 7.1 (Measurable sets and Lebesgue measure axioms): for n ∈ ℕ, a collection M ⊆ 𝒫(ℝ^n) and a function m : M → [0, +∞] (modeled here as m : Set (Fin n → ℝ) → ENNReal) satisfy: (i) every open set belongs to M; (ii) M is closed under complements; (iv) M is closed under countable unions and countable intersections; (v) m(∅) = 0; (vi) 0 ≤ m(Ω) ≤ +∞ for all Ω ∈ M; (xi) countable additivity on pairwise disjoint measurable families; (xii) m([0,1]^n) = 1; (xiii) translation invariance: x + Ω is measurable and has the same measure.

Equations

• One or more equations did not get rendered due to their size.

theorem exists_lebesgue_measure_axioms (n : ℕ) : ∃ (M : Set (Set (Fin n → ℝ))) (m : Set (Fin n → ℝ) → ENNReal), IsLebesgueMeasureAxioms n M m

Theorem 7.1 (Existence of Lebesgue measure): for each dimension n, there exist a σ-algebra M ⊆ 𝒫(ℝ^n) and a function m : M → [0,+∞] (modeled as m : Set (Fin n → ℝ) → ENNReal) satisfying the Borel property, complementarity, closure under countable unions and intersections, m(∅) = 0, positivity, countable additivity on pairwise disjoint families, normalization m([0,1]^n) = 1, and translation invariance.