Theorems · Definition · measure theory

MeasureTheory.MeasuredSets

{α : Type u_1} → [mα : MeasurableSpace α] → MeasureTheory.Measure α → Type u_1

The subtype of all measurable sets. We denote it as MeasuredSets μ, with an explicit but unused parameter μ, to be able to define a distance on it given by edist s t = μ (s ∆ t)

Defined in

Mathlib.MeasureTheory.Measure.MeasuredSets

Cited by

9 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

MeasurableSpace