maximum_mono

Mathlib.Data.List.MinMax

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

English

If l1 is a subset of l2, then the maximum of l1 is less than or equal to the maximum of l2.

Русский

Если l1 содержится в l2, то максимум l1 не превосходит максимум l2.

LaTeX

$$$l_1 \\subseteq l_2 \\Rightarrow \\max(l_1) \\le \\max(l_2)$$$

Lean4

theorem maximum_mono {l₁ l₂ : List α} (h : l₁ ⊆ l₂) : l₁.maximum ≤ l₂.maximum :=
  maximum_le_of_forall_le fun _ ↦ (le_maximum_of_mem' <| h ·)

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

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

Разделы

Аффилиация

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