min_assoc — Mathlib

English

min is associative: min(min(a,b),c) = min(a, min(b,c)).

Русский

min ассоциативен: min(min(a,b),c) = min(a, min(b,c)).

LaTeX

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

Lean4

theorem min_assoc (a b c : α) : min (min a b) c = min a (min b c) :=
  by
  apply eq_min
  · apply le_trans (min_le_left ..) (min_le_left ..)
  · apply le_min
    · apply le_trans (min_le_left ..) (min_le_right ..)
    · apply min_le_right
  · intro d h₁ h₂; apply le_min
    · apply le_min h₁; apply le_trans h₂; apply min_le_left
    · apply le_trans h₂; apply min_le_right

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