nhdsWithin_biUnion — Mathlib

English

For a finite index set I and a family of sets s_i, the neighborhood at a equals the supremum over i of nhdsWithin a s_i, taken over i in I.

Русский

Для конечного множества индексов I и семейства множеств s_i окрестность в a равняется наибольшему объединению (супремуму) 𝓝[s_i] a по i ∈ I.

LaTeX

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

Lean4

theorem nhdsWithin_biUnion {ι} {I : Set ι} (hI : I.Finite) (s : ι → Set α) (a : α) :
    𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a := by
  induction I, hI using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hT => simp only [hT, nhdsWithin_union, iSup_insert, biUnion_insert]

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