max_eq_left

Mathlib.Order.Defs.LinearOrder

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

English

If b ≤ a, then max(a,b) = a.

Русский

Если b ≤ a, то max(a,b) = a.

LaTeX

$$(b \le a) \Rightarrow \max(a,b) = a$$

Lean4

theorem max_eq_left (h : b ≤ a) : max a b = a := by apply Eq.symm; apply eq_max (le_refl _) h; intros; assumption

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

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

Разделы

Аффилиация

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