maximum_cons — Mathlib

English

Let α be a linearly ordered set. For any a ∈ α and any list l, the maximum of a :: l equals max(a, maximum l).

Русский

Пусть α упорядочено линейно. Для любого a и списка l максимум конcа a :: l равен max(a, максимум l).

LaTeX

$$$\\max(a \\,::\\, l) = \\max(a, \\max l)$$$

Lean4

theorem maximum_cons (a : α) (l : List α) : maximum (a :: l) = max ↑a (maximum l) :=
  List.reverseRecOn l (by simp) fun tl hd ih => by rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]

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