Theorems · Definition · general topology

ContinuousMap.restrict

{α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → (s : Set α) → C(α, β) → C(↑s, β)

The restriction of a continuous function α → β to a subset s of α.

Defined in

Mathlib.Topology.ContinuousMap.Basic

Cited by

61 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace