succ_min

Mathlib.Order.SuccPred.Archimedean

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

English

The successor operator preserves the minimum: succ(min(a,b)) = min(succ(a), succ(b)).

Русский

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

LaTeX

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

Lean4

theorem succ_min (a b : α) : succ (min a b) = min (succ a) (succ b) :=
  succ_mono.map_min

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

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

Разделы

Аффилиация

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