Ico_succ_left_eq_Ioo — Mathlib

English

Let α be a linearly ordered, locally finite, successor-ordered type. For all a,b ∈ α, the interval Ico (succ a) b coincides with Ioo a b.

Русский

Пусть α — линейно упорядоченный, локально конечный порядок с операцией successor. Для любых a, b ∈ α выполняется равенство Ico (succ a) b = Ioo a b.

LaTeX

$$$\forall a,b:\, \alpha,\ Ico(\text{succ}\,a)\,b = Ioo\,a\,b$$$

Lean4

theorem Ico_succ_left_eq_Ioo (a b : α) : Ico (succ a) b = Ioo a b :=
  coe_injective <| by simpa using Set.Ico_succ_left_eq_Ioo _ _

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