English
A variant form of sum_Ico_le_sum: under the same hypotheses, the conclusion holds with the corresponding indexed bounds.
Русский
Вариант формы неравенства для суммы Ico, аналогично предыдущему случаю.
LaTeX
$$$\text{(неформально)} \; \text{сохранение неравенства в варианте Ico}$$$
Lean4
/-- Sharp lower bound for the sum of a finset of integers that is bounded below, `range` version. -/
theorem sum_range_le_sum {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, c ≤ x) : ∑ n ∈ range #s, (c + n) ≤ ∑ x ∈ s, x :=
by
convert sum_Ico_le_sum hs
refine sum_nbij (c + ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)
· intro x mx; rw [mem_Ico]; dsimp only; rw [mem_range] at mx; cutsat
· intro x mx y my (h : c + x = c + y); cutsat
· intro x mx; simp_rw [coe_range, Set.mem_image, Set.mem_Iio]
rw [mem_coe, mem_Ico] at mx
use (x - c).toNat; omega
