English
If a ≤ x for some x ∈ l, then a ≤ l.foldr max b for any b.
Русский
Если a ≤ x для некоторого x ∈ l, тогда a ≤ l.foldr max b для любого b.
LaTeX
$$$\\forall {\\alpha} [\\mathrm{LinearOrder}(\\alpha)], {\\forall l : \\List(\\alpha)} {\\forall a x : \\alpha} (hx : x \\in l) (h : a \\le x) : a \\le l.foldr max b$$$
Lean4
/-- If `a ≤ x` for some `x` in the list `l`, and `b : α`, then `a ≤ l.foldr max b`. -/
theorem le_max_of_le' {l : List α} {a x : α} (b : α) (hx : x ∈ l) (h : a ≤ x) : a ≤ l.foldr max b := by
induction l with
| nil => exact absurd hx List.not_mem_nil
| cons y l IH =>
simp only [List.foldr]
obtain rfl | hl := mem_cons.mp hx
· exact le_max_of_le_left h
· exact le_max_of_le_right (IH hl)
