not_equitableOn — Mathlib

English

EquitableOn(s,f) fails exactly when there exist two elements a,b ∈ s with f(b) + 1 < f(a).

Русский

EquitableOn(s,f) неверно тогда и только тогда, когда существуют элементы a,b ∈ s такие, что f(b) + 1 < f(a).

LaTeX

$$$$ \\neg \\mathrm{EquitableOn}(s,f) \\iff \\exists a \\in s, \\exists b \\in s,\\ f(b)+1 < f(a). $$$$

Lean4

@[simp]
theorem not_equitableOn : ¬s.EquitableOn f ↔ ∃ a ∈ s, ∃ b ∈ s, f b + 1 < f a := by simp [EquitableOn]

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