Theorems · Theorem · measure theory

VitaliFamily.measurableSet

∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (self : VitaliFamily μ) (x : X), ∀ s ∈ self.setsAt x, MeasurableSet s

All sets of the family are measurable.

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

2 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

PseudoMetricSpace