nhdsGT_sup_nhdsWithin_singleton — Mathlib

English

In a linearly ordered space, the join of nhds-within (a, ∞) and nhds-within ({a}) equals nhds-within ([a, ∞)) at a.

Русский

В линейно упорядоченном пространстве сумма (слияние) nhds внутри (а, ∞) и nhds внутри {a} равна nhds внутри ([a, ∞)) в точке a.

LaTeX

$$$\\mathcal{N}_{>a} \\uparrow \\mathcal{N}_{\\{a\\}}(a) = \\mathcal{N}_{\\ge a}(a)$$$

Lean4

theorem nhdsGT_sup_nhdsWithin_singleton (a : α) : 𝓝[>] a ⊔ 𝓝[{ a }] a = 𝓝[≥] a := by
  simp only [union_singleton, Ioi_insert, ← nhdsWithin_union]

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