nhdsWithin_sUnion — Mathlib

English

If S is a finite set of subsets of α, the neighborhood at a with respect to the union ⋃ S equals the supremum over s ∈ S of nhdsWithin a s.

Русский

Если S — конечное множество подмножеств пространства, то окрестность в a относительно ⋃ S равна наибольшему объединению по s ∈ S окрестностей 𝓝[s] a.

LaTeX

$$$$ 𝓝[⋃_{s ∈ S} s] a = \\bigvee_{s ∈ S} 𝓝[s] a $$$$

Lean4

theorem nhdsWithin_sUnion {S : Set (Set α)} (hS : S.Finite) (a : α) : 𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a := by
  rw [sUnion_eq_biUnion, nhdsWithin_biUnion hS]

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