tsub_add_eq_max

Mathlib.Algebra.Order.Sub.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem tsub_add_eq_max : a - b + b = max a b :=
  by
  rcases le_total a b with h | h
  · rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
  · rw [max_eq_left h, tsub_add_cancel_of_le h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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