Ici_mem_nhdsSet_Ico — Mathlib

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

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