Theorems · Definition · general topology

SeqContinuous

{X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop

A function between topological spaces is sequentially continuous if it commutes with limit of convergent sequences.

Defined in

Mathlib.Topology.Defs.Sequences

Cited by

7 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace