IccIcoLems

theorem Icc_succ (n : ℕ) : Finset.Icc (-(↑n + 1)) (↑n + 1) = Finset.Icc (-↑n) ↑n ∪ {-(↑n + 1), ↑n + 1}

theorem trex (f : ℤ → ℂ) (N : ℕ) (hn : 1 ≤ N) : ∑ m ∈ Finset.Icc (-↑N) ↑N, f m = f ↑N + f (-↑N) + ∑ m ∈ Finset.Icc (-(↑N - 1)) (↑N - 1), f m

theorem Icc_sum_even (f : ℤ → ℂ) (hf : ∀ (n : ℤ), f n = f (-n)) (N : ℕ) : ∑ m ∈ Finset.Icc (-↑N) ↑N, f m = 2 * ∑ m ∈ Finset.range (N + 1), f ↑m - f 0

theorem verga2 : Filter.Tendsto (fun (N : ℕ) => Finset.Icc (-↑N) ↑N) Filter.atTop Filter.atTop

theorem int_add_abs_self_nonneg (n : ℤ) : 0 ≤ n + |n|

theorem verga : Filter.Tendsto (fun (N : ℕ) => Finset.Ico (-↑N) ↑N) Filter.atTop Filter.atTop

theorem fsb (b : ℕ) : Finset.Ico (-(↑b + 1)) (↑b + 1) = Finset.Ico (-↑b) ↑b ∪ {-(↑b + 1), ↑b}