insert_Icc_pred_right_eq_Icc — Mathlib

English

If a ≤ b, then inserting b into the closed interval Icc(a, pred(b)) yields Icc(a, b).

Русский

Пусть a ≤ b. Вставка b в замкнутый интервал Icc(a, pred(b)) дает Icc(a, b).

LaTeX

$$$\operatorname{insert}\ b\ (\mathrm{Icc}\ a\ (\operatorname{pred} b)) = \mathrm{Icc}\ a\ b$$$

Lean4

theorem insert_Icc_pred_right_eq_Icc (h : a ≤ b) : insert b (Icc a (pred b)) = Icc a b := by ext x;
  simp [or_and_left, ← le_iff_eq_or_le_pred]; simp_all

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