Iic_mem_nhdsSet_Icc

Mathlib.Topology.Order.NhdsSet

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

English

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

Русский

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

LaTeX

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

Lean4

theorem Iic_mem_nhdsSet_Icc (h : b < c) : Iic c ∈ 𝓝ˢ (Icc a b) :=
  mem_of_superset (Iio_mem_nhdsSet_Icc h) Iio_subset_Iic_self

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

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

Разделы

Аффилиация

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