English
EquitableOn(s,f) is equivalent to the existence of a bound b ∈ ℕ such that for all a ∈ s, b ≤ f(a) ≤ b+1.
Русский
EquitableOn(s,f) эквивалентно существованию границы b ∈ ℕ such that ∀ a ∈ s, b ≤ f(a) ≤ b+1.
LaTeX
$$$s.\mathrm{EquitableOn} f \iff \exists b \in \mathbb{N}, \forall a \in s, b \le f(a) \land f(a) \le b+1$$$
Lean4
theorem equitableOn_iff_exists_le_le_add_one {s : Set α} {f : α → ℕ} :
s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1 :=
by
refine ⟨?_, fun ⟨b, hb⟩ x y hx hy => (hb x hx).2.trans (add_le_add_right (hb y hy).1 _)⟩
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
· simp
intro hs
by_cases h : ∀ y ∈ s, f x ≤ f y
· exact ⟨f x, fun y hy => ⟨h _ hy, hs hy hx⟩⟩
push_neg at h
obtain ⟨w, hw, hwx⟩ := h
refine ⟨f w, fun y hy => ⟨Nat.le_of_succ_le_succ ?_, hs hy hw⟩⟩
rw [(Nat.succ_le_of_lt hwx).antisymm (hs hx hw)]
exact hs hx hy
