English
Let l be a finite list in a linear order. The maximum of l equals m if and only if m is in l and every element of l is ≤ m.
Русский
Пусть l — конечный список в линейном порядке. максимум l равен m тогда и только если m ∈ l и каждый элемент l ≤ m.
LaTeX
$$$\\max(l) = m \\iff \\bigl(m \\in l \\land \\forall a \\in l, a \\le m\\bigr)$$$
Lean4
theorem maximum_eq_coe_iff : maximum l = m ↔ m ∈ l ∧ ∀ a ∈ l, a ≤ m :=
by
rw [maximum, ← WithBot.some_eq_coe, argmax_eq_some_iff]
simp only [id_eq, and_congr_right_iff, and_iff_left_iff_imp]
intro _ h a hal hma
rw [_root_.le_antisymm hma (h a hal)]