fold_min_lt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem fold_min_lt : 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_lt_iff

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