Icc_mem_nhdsLE

Mathlib.Topology.Order.OrderClosed

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

English

If a < b in α, then the closed interval Icc(a,b) is a neighborhood of b within the lower-closed ray {x ≤ b}.

Русский

Если a < b в α, то замкнутый интервал Icc(a,b) является окрестностью точки b внутри множества {x ≤ b}.

LaTeX

$$$ a < b \implies Icc(a,b) \in 𝓝[≤] b $$$

Lean4

theorem Icc_mem_nhdsLE (H : a < b) : Icc a b ∈ 𝓝[≤] b :=
  Icc_mem_nhdsLE_of_mem ⟨H, le_rfl⟩

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

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

Разделы

Аффилиация

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