Theorems · Definition · general topology

ContinuousAt

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

A function between topological spaces is continuous at a point x₀ if f x tends to f x₀ when x tends to x₀.

Defined in

Mathlib.Topology.Defs.Filter

Cited by

697 results in Mathlib

Foundations

Depth 19 from the axioms, rests on 95 definitions · uses propext, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace