pred_max

Mathlib.Order.SuccPred.Archimedean

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

English

The predecessor operator distributes over the maximum: pred(max(a,b)) = max(pred(a), pred(b)).

Русский

Оператор предшествования распределяется по максимуму: pred(max(a,b)) = max(pred(a), pred(b)).

LaTeX

$$$ \forall a,b,\ pred(\max(a,b)) = \max(pred(a), pred(b)).$$$

Lean4

theorem pred_max (a b : α) : pred (max a b) = max (pred a) (pred b) :=
  pred_mono.map_max

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

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

Разделы

Аффилиация

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