minimum_concat — Mathlib

English

Let α be a linearly ordered set. For any a ∈ α and any list l, the minimum of l concatenated with [a] equals the minimum of the two minima: min(l ++ [a]) = min(minimum l, a).

Русский

Пусть α упорядочено линейно. Для любого a и любого списка l выполняется минимум конкатенации l с [a]: min(l ++ [a]) = min(minimum l, a).

LaTeX

$$$\\min(l \\,+\\ [a]) = \\min(\\min(l), a)$$$

Lean4

theorem minimum_concat (a : α) (l : List α) : minimum (l ++ [a]) = min (minimum l) a :=
  @maximum_concat αᵒᵈ _ _ _

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