Ico_succ_left_eq_Ioo — Mathlib

English

For any a,b in a linear order with SuccOrder, Ico(succ a, b) equals Ioo(a,b); in particular, if a is maximal the left-hand side is empty and matches the right-hand side.

Русский

Для любых a,b в линейном порядке с порядком перехода, множество Ico(succ a, b) равно Ioo(a,b); если a максимален, левая часть пустая и совпадает с правой.

LaTeX

$$$\\mathrm{Ico}(\\mathrm{Order.succ}\,a, b) = \\mathrm{Ioo}(a,b)$$$

Lean4

theorem Ico_succ_left_eq_Ioo (a b : α) : Ico (succ a) b = Ioo a b :=
  by
  by_cases ha : IsMax a
  · rw [Ico_eq_empty (ha.mono <| le_succ _).not_lt, Ioo_eq_empty ha.not_lt]
  · ext x
    rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]

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