case intro
y : ℝ*
r s : ℝ
hys : IsSt y s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : IsSt (ofSeq x) r
⊢ IsSt (Germ.map₂ f (ofSeq x) y) (f r s)
x y : ℝ*
r s : ℝ
hxr : IsSt x r
hys : IsSt y s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
⊢ IsSt (Germ.map₂ f x y) (f r s)
rcases ofSeq_surjective x with ⟨x, rfl⟩
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : IsSt (ofSeq x) r
y : ℕ → ℝ
hys : IsSt (ofSeq y) s
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
case intro
y : ℝ*
r s : ℝ
hys : IsSt y s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : IsSt (ofSeq x) r
⊢ IsSt (Germ.map₂ f (ofSeq x) y) (f r s)
rcases ofSeq_surjective y with ⟨y, rfl⟩
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : IsSt (ofSeq x) r
y : ℕ → ℝ
hys : IsSt (ofSeq y) s
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
rw [isSt_ofSeq_iff_tendsto] at hxr hys
no goals
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (hxr.prod_mk_nhds hys)