insert_Icc_right_eq_Icc_succ — Mathlib

English

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

Русский

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

LaTeX

$$$(a,b)\in α,\ a \le \mathrm{succ}(b) \Rightarrow \mathrm{insert}(\mathrm{succ}(b), \mathrm{Icc}(a,b)) = \mathrm{Icc}(a, \mathrm{succ}(b))$$$

Lean4

theorem insert_Icc_right_eq_Icc_succ (h : a ≤ succ b) : insert (succ b) (Icc a b) = Icc a (succ b) :=
  coe_injective <| by simpa using Set.insert_Icc_right_eq_Icc_succ h

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