Theorems · Theorem · measure theory

VitaliFamily.tendsto_filterAt_iff

∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) {ι : Type u_2} {l : Filter ι} {f : ι → Set X} {x : X},
  Filter.Tendsto f l (v.filterAt x) ↔
    (∀ᶠ (i : ι) in l, f i ∈ v.setsAt x) ∧ ∀ ε > 0, ∀ᶠ (i : ι) in l, f i ⊆ Metric.closedBall x ε

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

5 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace