English
If x ∈ l, there is an a with a ≤ x and hence a ≤ foldr max ⊥ over l.
Русский
Если x ∈ l, существует a such that a ≤ x, и тогда a ≤ foldr max ⊥ над l.
LaTeX
$$$\\forall {\\alpha} [\\mathrm{LinearOrder}(\\alpha)] [\\mathrm{OrderBot}(\\alpha)], {\\forall l : \\List(\\alpha)} {\\forall x : \\alpha}, x \\in l \\Rightarrow \\mathrm{foldr}(\\max) \\bot \\ge x$$$
Lean4
theorem le_max_of_le {l : List α} {a x : α} (hx : x ∈ l) (h : a ≤ x) : a ≤ l.foldr max ⊥ := by
induction l with
| nil => exact absurd hx not_mem_nil
| cons y l IH =>
obtain hl | hl := hx
· simp only [foldr]
exact le_max_of_le_left h
· exact le_max_of_le_right (IH (by assumption))
