case intro
r s : ℝ
f : ℕ → ℝ
hr : IsSt (ofSeq f) r
hs : IsSt (ofSeq f) s
⊢ r = s
x : ℝ*
r s : ℝ
hr : IsSt x r
hs : IsSt x s
⊢ r = s
rcases ofSeq_surjective x with ⟨f, rfl⟩
case intro
r s : ℝ
f : ℕ → ℝ
hr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
hs : Tendsto f (↑(hyperfilter ℕ)) (𝓝 s)
⊢ r = s
case intro
r s : ℝ
f : ℕ → ℝ
hr : IsSt (ofSeq f) r
hs : IsSt (ofSeq f) s
⊢ r = s
rw [isSt_ofSeq_iff_tendsto] at hr hs
no goals
case intro
r s : ℝ
f : ℕ → ℝ
hr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
hs : Tendsto f (↑(hyperfilter ℕ)) (𝓝 s)
⊢ r = s
exact tendsto_nhds_unique hr hs