nhdsWithin_union — Mathlib

English

Let a be a point in a topological space and s, t be subsets of the space. Then the neighborhood filter of a within s ∪ t is the supremum of the neighborhood filters within s and within t.

Русский

Пусть a — точка в топологическом пространстве, пусть s и t — подмножества. Тогда окрестностный фильтр a внутри s ∪ t равен наибольшему объединению окрестностных фильтров внутри s и внутри t.

LaTeX

$$$$ \\mathcal{N}_{s \\cup t}(a) = \\mathcal{N}_{s}(a) \\sqcup \\mathcal{N}_{t}(a) $$$$

Lean4

theorem nhdsWithin_union (a : α) (s t : Set α) : 𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a :=
  by
  delta nhdsWithin
  rw [← inf_sup_left, sup_principal]

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