Icc_mem_nhdsGE

Mathlib.Topology.Order.OrderClosed

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

English

If a < b, then Icc(a,b) is a neighborhood of a from above: Icc(a,b) ∈ 𝓝[≥] a.

Русский

Если a < b, то Icc(a,b) является окрестностью сверху точки a.

LaTeX

$$$\text{If } a < b,\; Icc(a,b) \in 𝓝_{\ge a}(a).$$$

Lean4

theorem Icc_mem_nhdsGE (H : a < b) : Icc a b ∈ 𝓝[≥] a :=
  Icc_mem_nhdsGE_of_mem ⟨le_rfl, H⟩

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

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

Разделы

Аффилиация

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