fold_max_le — Mathlib

English

Let c ∈ β. For finite s and functions f: α → β, the fold of max with base b is bounded by c precisely when b ≤ c and every f(x) ≤ c for x ∈ s.

Русский

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

LaTeX

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

Lean4

theorem fold_max_le : 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_le_iff

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