insert_Icc_left_eq_Icc_sub_one — Mathlib

English

In the discrete order, inserting a-1 into Icc(a,b) yields Icc(a-1,b): Icc(a,b) ∪ {a-1} = Icc(a-1,b).

Русский

В дискретном порядке вставка a-1 в Icc(a,b) дает Icc(a-1,b).

LaTeX

$$$ \mathrm{Icc}(a,b) \cup \{a-1\} = \mathrm{Icc}(a-1,b)$$$

Lean4

theorem insert_Icc_left_eq_Icc_sub_one (h : a - 1 ≤ b) : insert (a - 1) (Icc a b) = Icc (a - 1) b := by
  simpa [← pred_eq_sub_one] using insert_Icc_left_eq_Icc_pred (pred_eq_sub_one a ▸ h)

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