nhdsSet_Ici — Mathlib

English

Under suitable hypotheses, the neighborhoods of the closed ray [a, ∞) decompose as the supremum of the neighborhood of a and the principal of the open ray (a, ∞).

Русский

При подходящих гипотезах окрестности луча [a, ∞) разлагаются как объединение (верхняя грань) окрестностей a и принципиального фильтра на (a, ∞).

LaTeX

$$$𝓝^{s}(Ici(a)) = 𝓝 a \;⊔\; 𝓟(Ioi(a))$$$

Lean4

theorem nhdsSet_Ici : 𝓝ˢ (Ici a) = 𝓝 a ⊔ 𝓟 (Ioi a) := by rw [← Ioi_insert, nhdsSet_insert, nhdsSet_Ioi]

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