maximum_concat — Mathlib

English

The maximum of a list built by appending a to l is the maximum of the previous maximum and a.

Русский

Максимум списка, полученного добавлением элемента a к списку l, равен максимальному элементу между текущим максимумом l и a.

LaTeX

$$$\operatorname{maximum}(l \;\text{++}\; [a]) = \max\big( \operatorname{maximum} l , a\big)$$$

Lean4

theorem maximum_concat (a : α) (l : List α) : maximum (l ++ [a]) = max (maximum l) a :=
  by
  simp only [maximum, argmax_concat, id]
  cases argmax id l
  · exact (max_eq_right bot_le).symm
  · simp [WithBot.some_eq_coe, max_def_lt, WithBot.coe_lt_coe]

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