vitaliFamily — Mathlib

English

If v is a Vitali family, then the Vitali filter has a HasBasis structure relative to setsAt and covering.

Русский

Если v — семейство Витали, то фильтр Витали имеет базисную структуру относительно setsAt и покрытия.

LaTeX

$$$\\text{Filter.HasBasis}(v)$-style statement for Vitali.$$

Lean4

theorem _root_.Filter.HasBasis.vitaliFamily {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {x : X}
    (h : (𝓝 x).HasBasis p s) : (v.filterAt x).HasBasis p (fun i ↦ {t ∈ v.setsAt x | t ⊆ s i}) := by
  simpa only [← Set.setOf_inter_eq_sep] using h.smallSets.inf_principal _

Похожие утверждения