le_minimum_of_forall_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem le_minimum_of_forall_le {b : WithTop α} (h : ∀ a ∈ l, b ≤ a) : b ≤ l.minimum := by
  induction l with
  | nil => simp
  | cons a l ih =>
    simp only [minimum_cons, le_min_iff]
    exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩

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