Icc_pred_right_eq_Ico — Mathlib

English

In a linearly ordered set with LocallyFiniteOrder, PredOrder, NoMinOrder, the closed interval [a, pred(b)] equals the half-open interval [a, b).

Русский

В линейном порядке с локально конечным порядком, PredOrder и отсутствием минимума верно: Icc(a, pred(b)) = Ico(a, b).

LaTeX

$$$ Icc(a, \operatorname{pred}(b)) = Ico(a,b) $$$

Lean4

theorem Icc_pred_right_eq_Ico (a b : α) : Icc a (pred b) = Ico a b :=
  coe_injective <| by simp

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