min_le_of_le' — Mathlib

English

For a list l and a, if x ∈ l and x ≤ a, then l.foldr min b ≤ a.

Русский

Для списка l и a, если x ∈ l и x ≤ a, то l.foldr min b ≤ a.

LaTeX

$$$\\forall {\\alpha} [\\mathrm{LinearOrder}(\\alpha)], {\\forall l : \\List(\\alpha)} {\\forall a x : \\alpha} (hx : x \\in l) (h : x \\le a) : \\mathrm{foldr}(\\min) b \\le a$$$

Lean4

theorem min_le_of_le' {l : List α} {a x : α} (b : α) (hx : x ∈ l) (h : x ≤ a) : l.foldr min b ≤ a :=
  @le_max_of_le' αᵒᵈ _ _ _ _ _ hx h

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