Theorems · Theorem · measure theory

Filter.HasBasis.vitaliFamily

∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) {ι : Sort u_2} {p : ι → Prop} {s : ι → Set X} {x : X},
  (nhds x).HasBasis p s → (v.filterAt x).HasBasis p fun i => {t | t ∈ v.setsAt x ∧ t ⊆ s i}

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace