case intro
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : IsSt (ofSeq g) r
⊢ IsSt (Germ.map f (ofSeq g)) (f r)
x : ℝ*
r : ℝ
hxr : IsSt x r
f : ℝ → ℝ
hf : ContinuousAt f r
⊢ IsSt (Germ.map f x) (f r)
rcases ofSeq_surjective x with ⟨g, rfl⟩
no goals
case intro
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : IsSt (ofSeq g) r
⊢ IsSt (Germ.map f (ofSeq g)) (f r)
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (isSt_ofSeq_iff_tendsto.1 hxr)