nhds_eq_nhdsWithin_sup_nhdsWithin

English

Let b be a point and I₁, I₂ sets with univ = I₁ ∪ I₂. Then the neighborhood filter at b equals the supremum of the neighborhood filters within I₁ and I₂.

Русский

Пусть b — точка, и I₁, I₂ — множества такие, что общее множество всего пространства равно I₁ ∪ I₂. Тогда окрестностный фильтр в b равен объединению (sup) окрестностных фильтров внутри I₁ и внутри I₂.

LaTeX

$$$$ \\mathcal{N}(b) = \\mathcal{N}_{b}^{\\text{Within } I_1} \\sqcup \\mathcal{N}_{b}^{\\text{Within } I_2} $$$$

Lean4

theorem nhds_eq_nhdsWithin_sup_nhdsWithin (b : α) {I₁ I₂ : Set α} (hI : Set.univ = I₁ ∪ I₂) :
    nhds b = nhdsWithin b I₁ ⊔ nhdsWithin b I₂ := by rw [← nhdsWithin_univ b, hI, nhdsWithin_union]

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