insert_Ico_left_eq_Ico_pred — Mathlib

English

For any a,b with NoMinOrder, inserting pred a into Ioc(a,b) yields Ioc(pred a, b).

Русский

Для любых a,b c NoMinOrder, вставка pred(a) в Ioc(a,b) дает Ioc(pred a, b).

LaTeX

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

Lean4

theorem insert_Ico_left_eq_Ico_pred (h : a ≤ b) : insert (pred a) (Ico a b) = Ico (pred a) b :=
  insert_Ico_left_eq_Ico_pred_of_not_isMin h (not_isMin _)

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