English
To prove that a function to a T1 space is continuous at a point x, it suffices to show that it has a limit y at x: Tendsto f (nhds x) (nhds y) implies ContinuousAt f x.
Русский
Чтобы доказать непрерывность функции в точке x, достаточно показать, что у функции есть предел y в x: Tendsto f (nhds x) (nhds y) приводит к ContinuousAt f x.
LaTeX
$$$\text{ Tendsto } f (\mathcal{N} x) (\mathcal{N} y) \Rightarrow \text{ ContinuousAt } f x$$$
Lean4
/-- To prove a function to a `T1Space` is continuous at some point `x`, it suffices to prove that
`f` admits *some* limit at `x`. -/
theorem continuousAt_of_tendsto_nhds [TopologicalSpace Y] [T1Space Y] {f : X → Y} {x : X} {y : Y}
(h : Tendsto f (𝓝 x) (𝓝 y)) : ContinuousAt f x := by rwa [ContinuousAt, eq_of_tendsto_nhds h]
