minimum_cons

Mathlib.Data.List.MinMax

URI: https://scilib.ai/kg/mathlib#List.minimum_cons

English

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

Русский

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

LaTeX

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

Lean4

theorem minimum_cons (a : α) (l : List α) : minimum (a :: l) = min ↑a (minimum l) :=
  @maximum_cons αᵒᵈ _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru