English
Let α be a linearly ordered topological space with order-closed topology. If a < b, then the closed ray [a, ∞) is a neighborhood of the half-open interval [b, c) in the topology on sets.
Русский
Пусть α — линейно упорядоченное топологическое пространство с топологией, совместимой с порядком. Если a < b, то луч [a, ∞) является окрестностью полузакрытого интервала [b, c) в топологии множеств.
LaTeX
$$$$\atri{Ici}{a} \in \mathcal{N}_{\mathrm{set}}(\mathrm{Ico}\, b\, c)$$$$
Lean4
theorem Ici_mem_nhdsSet_Ico (h : a < b) : Ici a ∈ 𝓝ˢ (Ico b c) :=
nhdsSet_mono Ico_subset_Icc_self <| Ici_mem_nhdsSet_Icc h