nhdsWithin_Ioc_eq_nhdsGT

Mathlib.Topology.Order.OrderClosed

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

English

For a < b, the neighborhood of a within Ioc a b equals the neighborhood within Ioi a.

Русский

Для a < b окружность a внутри Ioc a b равна окружности внутри Ioi a.

LaTeX

$$$a < b \rightarrow 𝓝[Ioc a b] a = 𝓝[Ioi a] a$$$

Lean4

@[simp]
theorem nhdsWithin_Ioc_eq_nhdsGT (h : a < b) : 𝓝[Ioc a b] a = 𝓝[>] a :=
  nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iic_mem_nhds h

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

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

Разделы

Аффилиация

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