equitableOn_iff_exists_eq_eq_add_one

English

Let S be a subset of a set A and f : A → N. Then S is equitable on f if and only if there exists a natural number b such that for every a ∈ S, either f(a) = b or f(a) = b + 1.

Русский

Пусть S ⊆ A и f : A → ℕ. Тогда S является справедливо распределённой по f тогда и только тогда, существует натуральное число b, для которого для каждого a ∈ S выполняется либо f(a) = b, либо f(a) = b + 1.

LaTeX

$$$$ \\mathrm{EquitableOn}(s,f) \\iff \\exists b \\in \\mathbb{N}, \\forall a \\in s,\\ f(a) \\in \\{b,b+1\\}. $$$$

Lean4

theorem equitableOn_iff_exists_eq_eq_add_one {s : Set α} {f : α → ℕ} :
    s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, f a = b ∨ f a = b + 1 := by
  simp_rw [equitableOn_iff_exists_le_le_add_one, Nat.le_and_le_add_one_iff]

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