Theorems · Theorem · measure theory

VitaliFamily.fineSubfamilyOn_iff_frequently

∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) {f : X → Set (Set X)} {s : Set X},
  v.FineSubfamilyOn f s ↔ ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace