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]