maximum_le_of_forall_le — Mathlib

English

Let α be a linearly ordered set. If every element of l is ≤ b, then the maximum of l is ≤ b.

Русский

Пусть α упорядочено линейно. Если каждый элемент списка l не превосходит b, то максимум списка l не превосходит b.

LaTeX

$$$\\left( \\forall a \\in l,\\ a \\le b \\right) \\Rightarrow \\max(l) \\le b$$$

Lean4

theorem maximum_le_of_forall_le {b : WithBot α} (h : ∀ a ∈ l, a ≤ b) : l.maximum ≤ b := by
  induction l with
  | nil => simp
  | cons a l ih =>
    simp only [maximum_cons, max_le_iff]
    exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩

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