Ico_mem_nhdsGT

Mathlib.Topology.Order.OrderClosed

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

English

If a < b, then Ico(a, b) is a neighborhood of a from the right.

Русский

Если a < b, то Ico(a, b) является окрестностью a справа.

LaTeX

$$$a < b \rightarrow Ico(a, b) \in 𝓝[>] a$$$

Lean4

theorem Ico_mem_nhdsGT (H : a < b) : Ico a b ∈ 𝓝[>] a :=
  Ico_mem_nhdsGT_of_mem ⟨le_rfl, H⟩

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

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

Разделы

Аффилиация

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