English
For a finite set S, EquitableOn(s,f) holds iff every a ∈ S has f(a) equal to the average over S or that average plus 1.
Русский
Для конечного множества S равномерность по f выполняется тогда и только тогда, когда у каждого a ∈ S значение f(a) равно среднему по S или среднему по S плюс 1.
LaTeX
$$$$ \\mathrm{EquitableOn}(s,f) \\iff \\forall a \\in s,\\ f(a) = \\frac{\\sum_{i\\in s} f(i)}{s.card} \\lor f(a) = \\frac{\\sum_{i\\in s} f(i)}{s.card} + 1. $$$$
Lean4
theorem equitableOn_iff :
EquitableOn (s : Set α) f ↔ ∀ a ∈ s, f a = (∑ i ∈ s, f i) / s.card ∨ f a = (∑ i ∈ s, f i) / s.card + 1 := by
simp_rw [equitableOn_iff_le_le_add_one, Nat.le_and_le_add_one_iff]
