Icc_mem_nhdsLT

Mathlib.Topology.Order.OrderClosed

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

English

If a < b, then Icc a b is a left-neighborhood of b: Icc a b ∈ 𝓝[<] b.

Русский

Если a < b, то Icc a b является левой окрестностью b: Icc a b ∈ 𝓝[<] b.

LaTeX

$$$(a

Lean4

theorem Icc_mem_nhdsLT (H : a < b) : Icc a b ∈ 𝓝[<] b :=
  Icc_mem_nhdsLT_of_mem ⟨H, le_rfl⟩

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

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

Разделы

Аффилиация

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