Theorems · Theorem · measure theory

VitaliFamily.filterAt_basis_closedBall

∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) (x : X),
  (v.filterAt x).HasBasis (fun x => 0 < x) fun x_1 => {t | t ∈ v.setsAt x ∧ t ⊆ Metric.closedBall x x_1}

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace