Iio_subset_Iic_iff

Mathlib.Order.Interval.Set.LinearOrder

URI: https://scilib.ai/kg/mathlib#Set.Iio_subset_Iic_iff

English

Iio a ⊊ Iio b iff a < b.

Русский

Iio a ⊊ Iio b тогда и только тогда a < b.

LaTeX

$$$ Iio(a) \subset Iio(b) \iff a < b $$$

Lean4

@[simp]
theorem Iio_subset_Iic_iff [DenselyOrdered α] : Iio a ⊆ Iic b ↔ a ≤ b := by
  rw [← diff_eq_empty, Iio_diff_Iic, Ioo_eq_empty_iff, not_lt]

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

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

Разделы

Аффилиация

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