pred_succ_le

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.pred_succ_le

English

For a ≤ b, the half-open interval (pred a, b] equals {a} ∪ (a, b].

Русский

Для a ≤ b полувещественный интервал (pred a, b] равен {a} ∪ (a, b].

LaTeX

$$$ Ioc(\\mathrm{pred}\\ a)\\ b = \\mathrm{insert}\\ a\\ (Ioc\\ a\\ b) \\quad \\text{for } a \\le b $$$

Lean4

theorem pred_succ_le (a : α) : pred (succ a) ≤ a :=
  (wcovBy_succ _).pred_le

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru