Ioo_add_one_right_eq_Ioc — Mathlib

English

For all a, b in a linear ordered set, the open-open interval Ioo(a, b+1) equals the open-closed interval Ioc(a, b): Ioo(a, b+1) = Ioc(a, b).

Русский

Для всех a, b в линейно упорядоченном множество интервал Ioo(a, b+1) равен интервалу Ioc(a, b).

LaTeX

$$$Ioo(a,b+1) = Ioc(a,b)$$$

Lean4

theorem Ioo_add_one_right_eq_Ioc (a b : α) : Ioo a (b + 1) = Ioc a b := by
  simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc a b

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