max_le_of_forall_le — Mathlib

English

Let l be a multiset in a linear order with an upper bound n. Then the maximum (as a fold) is at most n: fold max bot l ≤ n.

Русский

Пусть l — мультимножество в линейном порядке с верхней границей n. Тогда максимум (по свертке) не превосходит n: max bot l ≤ n.

LaTeX

$$$ \text{Compute }\, \mathrm{fold}_{\mathrm{max}}(l) \le n$ under the assumptions; more precisely, $\max(\bot, l_1, l_2, \ldots) \le n$$$

Lean4

theorem max_le_of_forall_le {α : Type*} [LinearOrder α] [OrderBot α] (l : Multiset α) (n : α) (h : ∀ x ∈ l, x ≤ n) :
    l.fold max ⊥ ≤ n := by
  induction l using Quotient.inductionOn
  simpa using List.max_le_of_forall_le _ _ h

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