tsub_tsub_eq_min

Mathlib.Algebra.Order.Sub.Basic

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

English

For any a,b in α, a − (a − b) = min(a,b).

Русский

Для любых a,b в α выполняется a − (a − b) = min(a,b).

LaTeX

$$$a - (a - b) = \min(a,b)$$$

Lean4

theorem tsub_tsub_eq_min (a b : α) : a - (a - b) = min a b := by
  rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]

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

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

Разделы

Аффилиация

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