LimunderLems

theorem limUnder_add {α : Type u_1} [Preorder α] [Filter.atTop.NeBot] (f g : α → ℂ) (hf : CauchySeq f) (hg : CauchySeq g) : Filter.atTop.limUnder f + Filter.atTop.limUnder g = Filter.atTop.limUnder (f + g)

theorem limUnder_mul_const {α : Type u_1} [Preorder α] [Filter.atTop.NeBot] (f : α → ℂ) (hf : CauchySeq f) (c : ℂ) : c * Filter.atTop.limUnder f = Filter.atTop.limUnder (c • f)

theorem limUnder_sub {α : Type u_1} [Preorder α] [Filter.atTop.NeBot] (f g : α → ℂ) (hf : CauchySeq f) (hg : CauchySeq g) : Filter.atTop.limUnder f - Filter.atTop.limUnder g = Filter.atTop.limUnder (f - g)

theorem limUnder_congr_eventually (f g : ℕ → ℂ) (h : ∀ᶠ (n : ℕ) in Filter.atTop, f n = g n) (hf : CauchySeq f) (hg : CauchySeq g) : Filter.atTop.limUnder f = Filter.atTop.limUnder g

theorem tsum_limUnder_atTop (f : ℤ → ℂ) (hf : Summable f) : ∑' (n : ℤ), f n = Filter.atTop.limUnder fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, f n