lt_fold_max — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem lt_fold_max : c < s.fold max b f ↔ c < b ∨ ∃ x ∈ s, c < f x :=
  fold_op_rel_iff_or lt_max_iff

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