Iio_mem_nhdsSet_Iic_iff

Mathlib.Topology.Order.NhdsSet

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

English

If b < c, then Iio c is in nhdsSet(Iic a).

Русский

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

LaTeX

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

Lean4

theorem Iio_mem_nhdsSet_Iic_iff : Iio b ∈ 𝓝ˢ (Iic a) ↔ a < b :=
  Ioi_mem_nhdsSet_Ici_iff (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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