nhdsSet_iUnion — Mathlib

English

For a family of sets s i, the set-neighborhood-filter of their union equals the supremum of the set-neighborhood-filters of the pieces: 𝓝ˢ(⋃ i, s i) = ⨆ i, 𝓝ˢ(s i).

Русский

Для семейства множеств s_i фильтр окрестностей объединения равен верхней границе (объединению) фильтров окрестностей каждого члена: 𝓝ˢ(⋃ i, s i) = ⨆ i, 𝓝ˢ(s i).

LaTeX

$$$\\nhdsˢ(\\bigcup_i s_i) = \\bigsqcup_i (\\nhdsˢ (s_i))$$$

Lean4

theorem nhdsSet_iUnion {ι : Sort*} (s : ι → Set X) : 𝓝ˢ (⋃ i, s i) = ⨆ i, 𝓝ˢ (s i) := by
  simp only [nhdsSet, image_iUnion, sSup_iUnion (β := Filter X)]

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