theorem continuous_iff_seqContinuous_of_metricSpace {X : Type u} [MetricSpace X] {Y : Type v} [TopologicalSpace Y] {f : X → Y} : Continuous f ↔ SeqContinuous f

Fact 1.38: for a map from a metric space to a topological space, continuity is equivalent to sequential continuity; no Hausdorff assumption on the codomain is needed.