maximum_append — Mathlib

English

Let α be a linearly ordered set. For any lists l1, l2, the maximum of their concatenation equals the maximum of the maxima: (l1 ++ l2).maximum = max(l1.maximum, l2.maximum).

Русский

Пусть α упорядочено линейно. Максимум конкатенации двух списков равен максимуму их максимумов.

LaTeX

$$$ (l_1 \\,+\\ l_2).maximum = \\max(l_1.max, l_2.max) $$$

Lean4

theorem maximum_append (l₁ l₂ : List α) : (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum := by
  induction l₁ with
  | nil => simp
  | cons _ _ ih => rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]

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