nhdsWithin_Ioo_eq_nhdsGT

Mathlib.Topology.Order.OrderClosed

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem nhdsWithin_Ioo_eq_nhdsGT (h : a < b) : 𝓝[Ioo a b] a = 𝓝[>] a :=
  nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iio_mem_nhds h

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

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

Разделы

Аффилиация

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