Ioo_pred_right_eq_insert

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.Ioo_pred_right_eq_insert

← MathLib Explorer

English

For a < b, the open interval (pred a, b) equals {a} ∪ (a, b).

Русский

При a < b открытый интервал (pred a, b) равен {a} ∪ (a, b).

LaTeX

$$$ Ioo(\\mathrm{pred}\\ a)\\ b = \\mathrm{insert}\\ a\\ (Ioo\\ a\\ b) \\quad \\text{for } a < b $$$

Lean4

theorem Ioo_pred_right_eq_insert (h : a < b) : Ioo (pred a) b = insert a (Ioo a b) := by
  simp_rw [← Ioi_inter_Iio, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iio.2 h)]

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

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

Разделы

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

Аффилиация

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