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.

source
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

Instances For
source
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

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

The type of continuous maps from X to Y.

Equations
  • One or more equations did not get rendered due to their size.
source
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

Instances
source
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

source
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 := ⋯ }
Instances For
source
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 #

source
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' := ⋯ }
source
instance ContinuousMap.instContinuousMapClass {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
ContinuousMapClass C(X, Y) X Y
Equations
  • ⋯ = ⋯
source
@[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
source
instance ContinuousMap.instCanLiftForallCoeContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
CanLift (X → Y) C(X, Y) DFunLike.coe Continuous
Equations
  • ⋯ = ⋯
source
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
source
@[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
source
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
source
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
source
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 := ⋯ }
source
@[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'
source
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
source
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.

source
@[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
source
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.

source
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.

source
theorem ContinuousMap.coe_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
Function.Injective DFunLike.coe
source
@[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