Theorems · Definition · measure theory

VitaliFamily.filterAt

{X : Type u_1} →
  [inst : PseudoMetricSpace X] →
    {m0 : MeasurableSpace X} → {μ : MeasureTheory.Measure X} → VitaliFamily μ → X → Filter (Set X)

Given a vitali family v, then v.filterAt x is the filter on Set X made of those families that contain all sets of v.setsAt x of a sufficiently small diameter. This filter makes it possible to express limiting behavior when sets in v.setsAt x shrink to x.

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

49 results in Mathlib

Foundations

Depth 48 from the axioms · uses propext, Quot.sound

Assumes

PseudoMetricSpace