add_tsub_eq_max

Mathlib.Algebra.Order.Sub.Basic

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

English

a + (b − a) = max(a,b).

Русский

a + (b − a) = max(a,b).

LaTeX

$$$a + (b - a) = \max(a,b)$$$

Lean4

theorem add_tsub_eq_max : a + (b - a) = max a b := by rw [add_comm, max_comm, tsub_add_eq_max]

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

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

Разделы

Аффилиация

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