fold_min_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem fold_min_le : s.fold min b f ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c :=
  by
  change _ ≥ _ ↔ _
  apply fold_op_rel_iff_or
  intro x y z
  change _ ≤ _ ↔ _
  exact min_le_iff

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