max_le_of_forall_le — Mathlib

English

If every element x in l is ≤ a, then foldr max ⊥ over l is ≤ a.

Русский

Если каждый элемент x в l удовлетворяет x ≤ a, то foldr max ⊥ над l ≤ a.

LaTeX

$$$\\forall {\\alpha} [\\mathrm{LinearOrder}(\\alpha)] [\\mathrm{OrderBot}(\\alpha)], \\forall l : \\List(\\alpha), \\forall a : \\alpha, \\bigl(\\forall x \\in l, x \\le a\\bigr) \\Rightarrow \\mathrm{foldr}(\\max) \\bot \\ l \\le a$$$

Lean4

theorem max_le_of_forall_le (l : List α) (a : α) (h : ∀ x ∈ l, x ≤ a) : l.foldr max ⊥ ≤ a := by
  induction l with
  | nil => simp
  | cons y l IH => simpa [h y mem_cons_self] using IH fun x hx => h x <| mem_cons_of_mem _ hx

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