fold_max_lt — 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 fold_max_lt : s.fold max b f < c ↔ b < c ∧ ∀ x ∈ s, f x < c :=
  by
  change _ > _ ↔ _
  apply fold_op_rel_iff_and
  intro x y z
  change _ < _ ↔ _
  exact max_lt_iff

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