nhdsWithin_iUnion — Mathlib

English

If ι is finite, the neighborhood at a for the union of s_i over i in ι equals the supremum over i of nhdsWithin a s_i.

Русский

Если индексы i образуют конечно множество, окрестность в a для объединения s_i по i ∈ ι равна наибольшему объединению 𝓝[s_i] a по i.

LaTeX

$$$$ 𝓝[\\bigcup_{i} s_i] a = \\bigvee_{i} 𝓝[s_i] a $$$$

Lean4

theorem nhdsWithin_iUnion {ι} [Finite ι] (s : ι → Set α) (a : α) : 𝓝[⋃ i, s i] a = ⨆ i, 𝓝[s i] a := by
  rw [← sUnion_range, nhdsWithin_sUnion (finite_range s), iSup_range]

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