case intro
r : ℝ
f : ℕ → ℝ
⊢ IsSt (ofSeq f) r ↔ Germ.Tendsto (ofSeq f) (𝓝 r)
x : ℝ*
r : ℝ
⊢ IsSt x r ↔ Germ.Tendsto x (𝓝 r)
rcases ofSeq_surjective x with ⟨f, rfl⟩
no goals
case intro
r : ℝ
f : ℕ → ℝ
⊢ IsSt (ofSeq f) r ↔ Germ.Tendsto (ofSeq f) (𝓝 r)
exact isSt_ofSeq_iff_tendsto