Equivalence_of_Definitions_of_Continuous_Mapping_Point
Provedcontinuityproofwikitopology
A mapping between topological spaces is continuous at a point iff preimages of open neighborhoods are open neighborhoods.
Preamble
import Mathlib.Topology.Basic
Formal statement
theorem Equivalence_of_Definitions_of_Continuous_Mapping_Point {X Y : Type _} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (x : X) : ContinuousAt f x ↔ ∀ U : Set Y, IsOpen U → f x ∈ U → ∃ V : Set X, IsOpen V ∧ x ∈ V ∧ Set.MapsTo f V U := by sorrySource