Theorem: exercise3_3 (LeanCourse/Assignments/Assignment3.lean)

State before:
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
⊢ SequentialLimit s₂ a
Tactic:
sorry
State after:
no goals