insert_Icc_left_eq_Icc_pred — Mathlib

English

If pred(a) ≤ b, inserting pred(a) into Icc(a, b) yields Icc(pred(a), b).

Русский

Если pred(a) ≤ b, вставка pred(a) в Icc(a, b) дает Icc(pred(a), b).

LaTeX

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

Lean4

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

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