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

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

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

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

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