min_comm

Mathlib.Order.Defs.LinearOrder

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

English

min a b = min b a for all a,b.

Русский

min(a,b) = min(b,a) для всех a,b.

LaTeX

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

Lean4

theorem min_comm (a b : α) : min a b = min b a :=
  eq_min (min_le_right a b) (min_le_left a b) fun h₁ h₂ => le_min h₂ h₁

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

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

Разделы

Аффилиация

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