Continuous bundled maps

In this file we define the type ContinuousMap of continuous bundled maps.

We use the DFunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

structure ContinuousMap (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] : Type (max u_1 u_2)

The type of continuous maps from X to Y.

When possible, instead of parametrizing results over (f : C(X, Y)), you should parametrize over {F : Type*} [ContinuousMapClass F X Y] (f : F).

When you extend this structure, make sure to extend ContinuousMapClass.

• toFun : X → Y

  The function X → Y

• continuous_toFun : Continuous self.toFun

  Proposition that toFun is continuous

def «termC(_,_)» : Lean.ParserDescr

C(X, Y) is the type of continuous maps from X to Y.

Equations

• One or more equations did not get rendered due to their size.

class ContinuousMapClass (F : Type u_1) (X : outParam (Type u_2)) (Y : outParam (Type u_3)) [TopologicalSpace X] [TopologicalSpace Y] [FunLike F X Y] : Prop

ContinuousMapClass F X Y states that F is a type of continuous maps.

You should extend this class when you extend ContinuousMap.

• map_continuous (f : F) : Continuous ⇑f

  Continuity

@[reducible]

def ContinuousMap.ofClass {F : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) : C(X, Y)

Coerce a bundled morphism with a ContinuousMapClass instance to a ContinuousMap.

Equations

• ↑f = { toFun := ⇑f, continuous_toFun := ⋯ }

@[deprecated ContinuousMap.ofClass (since := "2026-10-14")]

def toContinuousMap {F : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) : C(X, Y)

Alias of ContinuousMap.ofClass.

---

Coerce a bundled morphism with a ContinuousMapClass instance to a ContinuousMap.

Equations

• @toContinuousMap = @ContinuousMap.ofClass

@[instance_reducible]

instance instCoeTCContinuousMap {F : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [FunLike F X Y] [ContinuousMapClass F X Y] : CoeTC F C(X, Y)

Equations

• instCoeTCContinuousMap = { coe := ContinuousMap.ofClass }

Continuous maps

@[instance_reducible, macro_inline]

instance ContinuousMap.instFunLike {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : FunLike C(X, Y) X Y

Equations

• ContinuousMap.instFunLike = { coe := ContinuousMap.toFun, coe_injective := ⋯ }

instance ContinuousMap.instContinuousMapClass {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : ContinuousMapClass C(X, Y) X Y

@[simp]

theorem ContinuousMap.toFun_eq_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} : f.toFun = ⇑f

instance ContinuousMap.instCanLiftForallCoeContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : CanLift (X → Y) C(X, Y) DFunLike.coe Continuous

def ContinuousMap.Simps.apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : X → Y

See note [custom simps projection].

Equations

• ContinuousMap.Simps.apply f = ⇑f

@[simp]

theorem ContinuousMap.coe_ofClass {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Type u_3} [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) : ⇑↑f = ⇑f

@[deprecated ContinuousMap.coe_ofClass (since := "2026-10-15")]

theorem ContinuousMap.coe_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Type u_3} [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) : ⇑↑f = ⇑f

Alias of ContinuousMap.coe_ofClass.

theorem ContinuousMap.coe_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Type u_3} [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) (x : X) : ↑f x = f x

theorem ContinuousMap.injective_ofClass {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Type u_3} [FunLike F X Y] [ContinuousMapClass F X Y] : Function.Injective ofClass

Coercion to a ContinuousMap is injective.

The unprimed version ContinuousMap.coe_injective is used for the coercion from C(X, Y) to X → Y.

@[deprecated ContinuousMap.injective_ofClass (since := "2026-10-15")]

theorem ContinuousMap.coe_injective' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Type u_3} [FunLike F X Y] [ContinuousMapClass F X Y] : Function.Injective ofClass

Alias of ContinuousMap.injective_ofClass.

---

Coercion to a ContinuousMap is injective.

The unprimed version ContinuousMap.coe_injective is used for the coercion from C(X, Y) to X → Y.

theorem ContinuousMap.ext {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (h : ∀ (a : X), f a = g a) : f = g

theorem ContinuousMap.ext_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} : f = g ↔ ∀ (a : X), f a = g a

def ContinuousMap.copy {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (f' : X → Y) (h : f' = ⇑f) : C(X, Y)

Copy of a ContinuousMap with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

• f.copy f' h = { toFun := f', continuous_toFun := ⋯ }

@[simp]

theorem ContinuousMap.coe_copy {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (f' : X → Y) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem ContinuousMap.copy_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (f' : X → Y) (h : f' = ⇑f) : f.copy f' h = f

theorem ContinuousMap.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : Continuous ⇑f

Deprecated. Use map_continuous instead.

theorem ContinuousMap.congr_fun {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (H : f = g) (x : X) : f x = g x

Deprecated. Use DFunLike.congr_fun instead.

theorem ContinuousMap.congr_arg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) {x y : X} (h : x = y) : f x = f y

Deprecated. Use DFunLike.congr_arg instead.

theorem ContinuousMap.coe_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : Function.Injective DFunLike.coe

@[simp]

theorem ContinuousMap.coe_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : Continuous f) : ⇑{ toFun := f, continuous_toFun := h } = f

instance ContinuousMap.instSubsingleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Subsingleton Y] : Subsingleton C(X, Y)

instance ContinuousMap.instSubsingletonOfIsEmpty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty X] : Subsingleton C(X, Y)