foldr_min_of_ne_nil — Mathlib

English

If l ≠ ∅, then the with-top variant of foldr min equals the minimum of l: withTop(l.foldr min ⊤) = l.minimum.

Русский

Если l ≠ ∅, то с вершиной (withTop) свёртка min по списку равна минимуму списка: withTop(l.foldr min ⊤) = l.minimum.

LaTeX

$$$\\forall {\\alpha} [\\mathrm{LinearOrder}(\\alpha)] [\\mathrm{OrderTop}(\\alpha)], {\\forall l : \\List(\\alpha)}, l \\neq \\emptyset \\Rightarrow \\uparrow(l.foldr min \\top) = l.minimum$$$

Lean4

@[simp]
theorem foldr_min_of_ne_nil (h : l ≠ []) : ↑(l.foldr min ⊤) = l.minimum :=
  @foldr_max_of_ne_nil αᵒᵈ _ _ _ h

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