Theorems · Theorem · measure theory

VitaliFamily.eventually_filterAt_mem_setsAt

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

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace