Theorems · Theorem · measure theory

VitaliFamily.FineSubfamilyOn.measure_diff_biUnion

Deprecated since 2026-06-03Use VitaliFamily.FineSubfamilyOn.measure_sdiff_biUnion instead.

∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s),
  μ (s \ ⋃ p ∈ h.index, h.covering p) = 0

Alias of VitaliFamily.FineSubfamilyOn.measure_sdiff_biUnion.

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

0 results in Mathlib

Foundations

Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpace