Ico_eq_Ioo_same_iff

Mathlib.Order.Interval.Set.Basic

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

English

Ico(a,b) equals Ioo(a,b) iff not (a < b).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ico_eq_Ioo_same_iff : Ico a b = Ioo a b ↔ ¬a < b :=
  eq_comm.trans Ioo_eq_Ico_same_iff

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

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

Разделы

Аффилиация

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