insert_Icc_left_eq_Icc_pred — Mathlib

English

If pred a ≤ b, then insert pred a into Icc a b equals Icc (pred a) b.

Русский

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

LaTeX

$$$(a,b)\in α,\ \mathrm{pred}(a) \le b \Rightarrow \mathrm{insert}(\mathrm{pred}(a), \mathrm{Icc}(a,b)) = \mathrm{Icc}(\mathrm{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 :=
  coe_injective <| by simpa using Set.insert_Icc_left_eq_Icc_pred h

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