Ioo_pred_left — Mathlib

English

Let α be a linear order with PredOrder and NoMinOrder. Then for all a,b ∈ α, the open interval (pred a, b) equals the half-open interval [a, b).

Русский

Пусть α — линейно упорядоченное множество с PredOrder и NoMinOrder. Тогда для любых a,b ∈ α выполняется равенство множеств: Ioo(pred a, b) = Ico(a, b).

LaTeX

$$$ \\mathrm{Ioo}(\\mathrm{pred}\\, a)\\, b = \\mathrm{Ico}\\ a\\ b $$$

Lean4

@[simp]
theorem Ioo_pred_left (a b : α) : Ioo (pred a) b = Ico a b :=
  Ioo_pred_left_of_not_isMin <| not_isMin _

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