Theorems · Inductive type · measure theory

MeasureTheory.SigmaFinite

{α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop

A measure μ is called σ-finite if there is a countable collection of sets { A i | i ∈ ℕ } such that μ (A i) < ∞ and ⋃ i, A i = s.

Defined in

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Cited by

526 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms