le_fold_min — Mathlib

English

Let c ∈ β. For a finite s ⊆ α, a function f: α → β, and a base b ∈ β, we have: c ≤ Finset.fold(min) with base b and map f over s if and only if c ≤ b and ∀ x ∈ s, c ≤ f(x).

Русский

Пусть c ∈ β. Для конечного множества s ⊆ α и функции f: α → β, и базового элемента b ∈ β: c ≤ свертка по min над s равносильно c ≤ b и для всех x ∈ s выполняется c ≤ f(x).

LaTeX

$$$$ c \\le \\mathrm{Finset.fold}(\\min)\\; b\\; f\\; s \\Longleftrightarrow c \\le b \\land \\forall x \\in s,\\; c \\le f(x). $$$$

Lean4

theorem le_fold_min : c ≤ s.fold min b f ↔ c ≤ b ∧ ∀ x ∈ s, c ≤ f x :=
  fold_op_rel_iff_and le_min_iff

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