Documentation

Mathlib.Topology.ContinuousMap.Defs

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 : XY

    The function X → Y

  • continuous_toFun : Continuous self.toFun

    Proposition that toFun is continuous

theorem ContinuousMap.continuous_toFun {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (self : C(X, Y)) :
Continuous self.toFun

Proposition that toFun is continuous

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] :

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

Instances
    theorem ContinuousMapClass.map_continuous {F : Type u_1} {X : outParam (Type u_2)} {Y : outParam (Type u_3)} :
    ∀ {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} {inst_2 : FunLike F X Y} [self : ContinuousMapClass F X Y] (f : F), Continuous f

    Continuity

    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)

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

    Equations
    • f = { toFun := f, continuous_toFun := }
    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 := toContinuousMap }

    Continuous maps #

    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' := }
    @[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 (XY) C(X, Y) DFunLike.coe Continuous
    Equations
    • =
    def ContinuousMap.Simps.apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) :
    XY

    See note [custom simps projection].

    Equations
    @[simp]
    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
    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.ext_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {g : C(X, Y)} :
    f = g ∀ (a : X), f a = g a
    theorem ContinuousMap.ext {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {g : C(X, Y)} (h : ∀ (a : X), f a = g a) :
    f = g
    def ContinuousMap.copy {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (f' : XY) (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' : XY) (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' : XY) (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)) :

    Deprecated. Use map_continuous instead.

    @[deprecated ContinuousMapClass.map_continuous]
    theorem ContinuousMap.continuous_set_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set C(X, Y)) (f : s) :
    Continuous f
    theorem ContinuousMap.congr_fun {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {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 : X} {y : X} (h : x = y) :
    f x = f y

    Deprecated. Use DFunLike.congr_arg instead.

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