insert_Ico_left_eq_Ico_pred_of_not_isMin

English

If a ≤ b and a is not a minimum, then inserting pred(a) into Ico(a, b) yields Ico(pred(a), b).

Русский

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

LaTeX

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

Lean4

theorem insert_Ico_left_eq_Ico_pred_of_not_isMin (h : a ≤ b) (ha : ¬IsMin a) :
    insert (pred a) (Ico a b) = Ico (pred a) b := by ext x;
  simp +contextual [or_and_left, pred_le_iff_eq_or_le, pred_lt_of_not_isMin_of_le ha h]

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