Icc_succ_pred_eq_Ioo — Mathlib

English

For a, b in a linearly ordered NoMinOrder with Succ and Pred, the closed-closed interval between succ a and pred b equals the open interval between a and b: Icc(succ a, pred b) = Ioo(a, b).

Русский

Для a, b в линейном порядке без минимума, интервал Icc(succ a, pred b) равен Ioo(a, b).

LaTeX

$$$\mathrm{Icc}(\mathrm{succ} a, \mathrm{pred} b) = \mathrm{Ioo}(a, b)$$$

Lean4

theorem Icc_succ_pred_eq_Ioo (a b : α) : Icc (succ a) (pred b) = Ioo a b :=
  by
  by_cases hb : IsMin b
  · rw [Icc_eq_empty, Ioo_eq_empty hb.not_lt]
    exact fun h ↦ not_isMin_succ _ <| hb.mono <| h.trans <| pred_le _
  · rw [Icc_pred_right_eq_Ico_of_not_isMin hb, Ico_succ_left_eq_Ioo]

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