Icc_pred_right_eq_Ico — Mathlib

English

For any a,b, Icc(a, pred(b)) = Ico(a, b) when there is no minimum element (i.e., pred(b) exists and b is not minimal).

Русский

Для любых a,b, Icc(a, pred(b)) = Ico(a, b) при отсутствии минимума (предшественник b существует и b не минимален).

LaTeX

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

Lean4

theorem Icc_pred_right_eq_Ico (a b : α) : Icc a (pred b) = Ico a b :=
  Icc_pred_right_eq_Ico_of_not_isMin (not_isMin _) _

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