minimum_anti

Mathlib.Data.List.MinMax

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

English

If l1 ⊆ l2, then the minimum of l2 is less than or equal to the minimum of l1.

Русский

Если l1 содержится в l2, то минимум l2 не больше минимума l1.

LaTeX

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

Lean4

theorem minimum_anti {l₁ l₂ : List α} (h : l₁ ⊆ l₂) : l₂.minimum ≤ l₁.minimum :=
  @maximum_mono αᵒᵈ _ _ _ h

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

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

Разделы

Аффилиация

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