le_fold_max — Mathlib

English

Let c ∈ β. Then c ≤ Finset.fold(max) with base b and map f over s holds iff c ≤ b or there exists x ∈ s with c ≤ f(x).

Русский

Пусть c ∈ β. Тогда c ≤ свертка по max над s равносильно c ≤ b или существует x ∈ s такое, что c ≤ f(x).

LaTeX

$$$$ c \\le \\mathrm{Finset.fold}(\\max)\\; b\\; f \\Longleftrightarrow c \\le b \\lor \\exists x \\in s,\\; c \\le f(x). $$$$

Lean4

theorem le_fold_max : c ≤ s.fold max b f ↔ c ≤ b ∨ ∃ x ∈ s, c ≤ f x :=
  fold_op_rel_iff_or le_max_iff

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