max_assoc — Mathlib

English

max(max(a,b), c) = max(a, max(b,c)) for all a,b,c in a linear order.

Русский

max(max(a,b), c) = max(a, max(b,c)) для всех a,b,c в линейном порядке.

LaTeX

$$$\max(\max(a,b), c) = \max(a, \max(b,c))$$$

Lean4

theorem max_assoc (a b c : α) : max (max a b) c = max a (max b c) :=
  by
  apply eq_max
  · apply le_trans (le_max_left a b) (le_max_left ..)
  · apply max_le
    · apply le_trans (le_max_right a b) (le_max_left ..)
    · apply le_max_right
  · intro d h₁ h₂; apply max_le
    · apply max_le h₁; apply le_trans (le_max_left _ _) h₂
    · apply le_trans (le_max_right _ _) h₂

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