Icc_sub_one_right_eq_Ico_of_not_isMin

English

If b is not a minimum, then the closed interval Icc(a, b-1) equals the half-open interval Ico(a, b): Icc(a, b-1) = Ico(a, b) (provided ¬IsMin b).

Русский

Если b не минимален, то [a, b-1] = [a, b) (при условии ¬IsMin b).

LaTeX

$$$\lnot\operatorname{IsMin}(b) \Rightarrow Icc(a,b-1) = Ico(a,b)$$$

Lean4

theorem Icc_sub_one_right_eq_Ico_of_not_isMin (hb : ¬IsMin b) (a : α) : Icc a (b - 1) = Ico a b := by
  simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico_of_not_isMin hb a

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