lt_fold_min — Mathlib

English

Let c ∈ β. Then c < Finset.fold(min) with base b and map f over s holds iff c < b and ∀ x ∈ s, c < f(x).

Русский

Пусть c ∈ β. Тогда c < свертка по min над s равносильно c < b и для каждого x ∈ s выполняется c < f(x).

LaTeX

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

Lean4

theorem lt_fold_min : c < s.fold min b f ↔ c < b ∧ ∀ x ∈ s, c < f x :=
  fold_op_rel_iff_and lt_min_iff

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