min_le_of_le — Mathlib

English

For a list l and a, if every x ∈ l satisfies x ≤ a, then l.foldr min ⊤ ≤ a.

Русский

Для списка l и элемента a, если каждый x ∈ l удовлетворяет x ≤ a, то l.foldr min ⊤ ≤ a.

LaTeX

$$$\\forall l : \\List(\\alpha), \\forall a : \\alpha, \\bigl(\\forall x \\in l, x \\le a\\bigr) \\Rightarrow \\mathrm{foldr}(\\min) \\top \\le a$$$

Lean4

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

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