Theorems · Definition · general topology

ContinuousOn

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

A function between topological spaces is continuous on a subset s when it's continuous at every point of s within s.

Defined in

Mathlib.Topology.Defs.Filter

Cited by

1,411 results in Mathlib

Foundations

Depth 50 from the axioms, rests on 543 definitions · uses propext, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace