le_min_of_forall_le — Mathlib

English

If for all x ∈ l we have a ≤ x, then a ≤ foldr min ⊤ over l.

Русский

Если для каждого x ∈ l выполняется a ≤ x, то a ≤ foldr min ⊤ над l.

LaTeX

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

Lean4

theorem le_min_of_forall_le (l : List α) (a : α) (h : ∀ x ∈ l, a ≤ x) : a ≤ l.foldr min ⊤ :=
  @max_le_of_forall_le αᵒᵈ _ _ _ _ h

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