limits

Stream: new members

[BANGJI HU]

import Mathlib.Tactic
import Mathlib.Data.Real.Sqrt

def sLim (x : ℕ → ℝ) (a : ℝ) : Prop :=
  ∀ ε, 0 < ε → ∃ N, ∀ n, N ≤ n → |x n - a| < ε

notation "limₙ " => sLim

lemma sLim_def (x : ℕ → ℝ) (a : ℝ) : limₙ x a ↔ ∀ ε, 0 < ε → ∃ N, ∀ n, N ≤ n → |x n - a| < ε:= by rfl

lemma sLim_const (b : ℝ) : limₙ (fun _ => b) b :=
by
rw [sLim_def]
intros ε hε
exists 0
intros n hn
ring_nf
simp only [abs_zero]
assumption
theorem sLim_mul_const_nonneg (hx : limₙ x a) (b : ℝ) (hb : 0 ≤ b) : limₙ (fun n => x n * b) (a * b) :=
by
  by_cases hbp : b = 0
    convert sLim_const 0
    rw [hbp]
    simp only [mul_zero]

[BANGJI HU]

can you tell me what to do at the case b=0