Icc_add_one_left_eq_Ioc — Mathlib

English

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

Русский

Для всех a, b в линейно упорядоченном множестве замкнутый интервал [a+1, b] равен полузакрытому интервалу (a, b], т.е. Icc(a+1, b) = Ioc(a, b).

LaTeX

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

Lean4

theorem Icc_add_one_left_eq_Ioc (a b : α) : Icc (a + 1) b = Ioc a b := by
  simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc a b

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