Ioi_mem_nhdsSet_Ici_iff

Mathlib.Topology.Order.NhdsSet

URI: https://scilib.ai/kg/mathlib#Ioi_mem_nhdsSet_Ici_iff

English

If a < b, then the open ray Ioi a lies in the nhdsSet of Icc b c.

Русский

Если a < b, то открытый луч Ioi a принадлежит nhdsSet(Icc(b,c)).

LaTeX

$$$(h : a < b) \Rightarrow Ioi(a) \in 𝓝^{s}(Icc(b,c))$$$

Lean4

@[simp]
theorem Ioi_mem_nhdsSet_Ici_iff : Ioi a ∈ 𝓝ˢ (Ici b) ↔ a < b := by rw [isOpen_Ioi.mem_nhdsSet, Ici_subset_Ioi]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru