Iio_mem_nhdsSet_Icc

Mathlib.Topology.Order.NhdsSet

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

English

If b < c, then Iio c lies in nhdsSet(Icc a b).

Русский

Если b < c, то Iio c ∈ nhdsSet(Icc a b).

LaTeX

$$$(h : b < c) \Rightarrow Iio(c) \in 𝓝^{s}(Icc(a,b))$$$

Lean4

theorem Iio_mem_nhdsSet_Icc (h : b < c) : Iio c ∈ 𝓝ˢ (Icc a b) :=
  nhdsSet_mono Icc_subset_Iic_self <| Iio_mem_nhdsSet_Iic h

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

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

Разделы

Аффилиация

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