eventually_filterAt_subset_of_nhds

English

If o is a neighborhood of x (i.e., o ∈ 𝓝 x), then for the Vitali filter at x, eventually every member t satisfies t ⊆ o.

Русский

Пусть o является окрестностью точки x (o ∈ 𝓝 x). Тогда для фильтра Витали в точке x верно, что для всех достаточно больших t: t ⊆ o.

LaTeX

$$$o \\in \\mathcal{N}(x) \\Rightarrow \\mathrm{Eventual}\\, (t \\subseteq o)\\ (v.filterAt x)$$$

Lean4

theorem eventually_filterAt_subset_of_nhds {x : X} {o : Set X} (hx : o ∈ 𝓝 x) : ∀ᶠ t in v.filterAt x, t ⊆ o :=
  (eventually_smallSets_subset.2 hx).filter_mono inf_le_left

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