minimum_append — Mathlib

English

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

Русский

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

LaTeX

$$$ (l_1 \\,+\\ l_2).minimum = \\min(l_1.minimum, l_2.minimum) $$$

Lean4

theorem minimum_append (l₁ l₂ : List α) : (l₁ ++ l₂).minimum = min l₁.minimum l₂.minimum :=
  @maximum_append αᵒᵈ _ _ _

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