Theorems · Inductive type · measure theory

MeasureTheory.Measure.FiniteSpanningSetsIn

{α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Set (Set α) → Type u_1

μ has finite spanning sets in C if there is a countable sequence of sets in C that have finite measures. This structure is a type, which is useful if we want to record extra properties about the sets, such as that they are monotone. SigmaFinite is defined in terms of this: μ is σ-finite if there exists a sequence of finite spanning sets in the collection of all measurable sets.

Defined in

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Cited by

23 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms