Ioo_eq_Ico_same_iff

Mathlib.Order.Interval.Set.Basic

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

← MathLib Explorer

English

Ioo(a,b) equals Ico(a,b) exactly when not (a < b).

Русский

Ioo(a,b) равно Ico(a,b) когда не выполняется a < b.

LaTeX

$$$ Ioo(a,b) = Ico(a,b) \iff \neg (a < b).$$$

Lean4

@[simp]
theorem Ioo_eq_Ico_same_iff : Ioo a b = Ico a b ↔ ¬a < b
    where
  mp h := by simpa using Set.ext_iff.mp h a
  mpr
    h := by
    rw [Ioo_eq_empty h, Ico_eq_empty h]
      -- Mirrored versions of the above for `simp`.

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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