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]