strictAnti_iff_forall_lt_insert — Mathlib

English

A function f is strictly antitone iff for all s and a not in s, f(insert a s) < f s.

Русский

Функция f строго антитонна тогда и только тогда, когда для каждого s и каждого a ∉ s выполняется f(insert a s) < f s.

LaTeX

$$$\\text{StrictAnti}(f) \\iff ∀ s, ∀ a; a \\notin s \\to f(\\mathrm{insert}\\ a\\ s) < f(s)$$$

Lean4

/-- A function `f` from `Finset α` is strictly antitone if and only if `f (insert a s) < f s` for
all `s` and `a ∉ s`. -/
theorem strictAnti_iff_forall_lt_insert : StrictAnti f ↔ ∀ s ⦃a⦄, a ∉ s → f (insert a s) < f s :=
  strictMono_iff_forall_lt_insert (β := βᵒᵈ)

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