succ_max

Mathlib.Order.SuccPred.Archimedean

URI: https://scilib.ai/kg/mathlib#succ_max

English

The successor operator preserves the maximum: succ(max(a,b)) = max(succ(a), succ(b)).

Русский

Оператор перехода к следующему элементу сохраняет максимум: succ(max(a,b)) = max(succ(a), succ(b)).

LaTeX

$$$ \forall a,b,\ \operatorname{succ}(\max(a,b)) = \max(\operatorname{succ}(a), \operatorname{succ}(b)).$$$

Lean4

theorem succ_max (a b : α) : succ (max a b) = max (succ a) (succ b) :=
  succ_mono.map_max

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

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

Разделы

Аффилиация

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