# Documentation

Mathlib.Topology.ContinuousFunction.Basic

# Continuous bundled maps #

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

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

structure ContinuousMap (α : Type u_1) (β : Type u_2) [] [] :
Type (max u_1 u_2)
• toFun : αβ

The function α → β

• continuous_toFun : Continuous s.toFun

Proposition that toFun is continuous

The type of continuous maps from α to β.

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

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

Instances For

The type of continuous maps from α to β.

Instances For
class ContinuousMapClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [] [] extends :
Type (max (max u_1 u_2) u_3)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• map_continuous : ∀ (f : F),

Continuity

ContinuousMapClass F α β states that F is a type of continuous maps.

You should extend this class when you extend ContinuousMap.

Instances
theorem map_continuousAt {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] (f : F) (a : α) :
ContinuousAt (f) a
theorem map_continuousWithinAt {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] (f : F) (s : Set α) (a : α) :
def toContinuousMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] (f : F) :
C(α, β)

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

Instances For
instance instCoeTCContinuousMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] :
CoeTC F C(α, β)

### Continuous maps #

instance ContinuousMap.toContinuousMapClass {α : Type u_1} {β : Type u_2} [] [] :
@[simp]
theorem ContinuousMap.toFun_eq_coe {α : Type u_1} {β : Type u_2} [] [] {f : C(α, β)} :
f.toFun = f
instance ContinuousMap.instCanLiftForAllContinuousMapCoeToFunLikeToContinuousMapClassContinuous {α : Type u_1} {β : Type u_2} [] [] :
CanLift (αβ) C(α, β) FunLike.coe Continuous
def ContinuousMap.Simps.apply {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) :
αβ

See note [custom simps projection].

Instances For
@[simp]
theorem ContinuousMap.coe_coe {α : Type u_1} {β : Type u_2} [] [] {F : Type u_5} [] (f : F) :
f = f
theorem ContinuousMap.ext {α : Type u_1} {β : Type u_2} [] [] {f : C(α, β)} {g : C(α, β)} (h : ∀ (a : α), f a = g a) :
f = g
def ContinuousMap.copy {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (f' : αβ) (h : f' = f) :
C(α, β)

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

Instances For
@[simp]
theorem ContinuousMap.coe_copy {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (f' : αβ) (h : f' = f) :
↑() = f'
theorem ContinuousMap.copy_eq {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (f' : αβ) (h : f' = f) :
= f
theorem ContinuousMap.continuous {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) :

Deprecated. Use map_continuous instead.

theorem ContinuousMap.continuous_set_coe {α : Type u_1} {β : Type u_2} [] [] (s : Set C(α, β)) (f : s) :
Continuous f
theorem ContinuousMap.continuousAt {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (x : α) :
ContinuousAt (f) x

Deprecated. Use map_continuousAt instead.

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

Deprecated. Use FunLike.congr_fun instead.

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

Deprecated. Use FunLike.congr_arg instead.

theorem ContinuousMap.coe_injective {α : Type u_1} {β : Type u_2} [] [] :
Function.Injective FunLike.coe
@[simp]
theorem ContinuousMap.coe_mk {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (h : ) :
↑() = f
theorem ContinuousMap.map_specializes {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) {x : α} {y : α} (h : x y) :
f x f y
@[simp]
theorem ContinuousMap.equivFnOfDiscrete_apply (α : Type u_1) (β : Type u_2) [] [] [] (f : C(α, β)) (a : α) :
↑() f a = f a
@[simp]
theorem ContinuousMap.equivFnOfDiscrete_symm_apply_apply (α : Type u_1) (β : Type u_2) [] [] [] (f : αβ) :
∀ (a : α), ↑(().symm f) a = f a
def ContinuousMap.equivFnOfDiscrete (α : Type u_1) (β : Type u_2) [] [] [] :
C(α, β) (αβ)

The continuous functions from α to β are the same as the plain functions when α is discrete.

Instances For
def ContinuousMap.id (α : Type u_1) [] :
C(α, α)

The identity as a continuous map.

Instances For
@[simp]
theorem ContinuousMap.coe_id (α : Type u_1) [] :
↑() = id
def ContinuousMap.const (α : Type u_1) {β : Type u_2} [] [] (b : β) :
C(α, β)

The constant map as a continuous map.

Instances For
@[simp]
theorem ContinuousMap.coe_const (α : Type u_1) {β : Type u_2} [] [] (b : β) :
↑() =
@[simp]
theorem ContinuousMap.constPi_apply (α : Type u_1) {β : Type u_2} [] :
= fun b =>
def ContinuousMap.constPi (α : Type u_1) {β : Type u_2} [] :
C(β, αβ)

Function.const α b as a bundled continuous function of b.

Instances For
instance ContinuousMap.instInhabitedContinuousMap (α : Type u_1) {β : Type u_2} [] [] [] :
@[simp]
theorem ContinuousMap.id_apply {α : Type u_1} [] (a : α) :
↑() a = a
@[simp]
theorem ContinuousMap.const_apply {α : Type u_1} {β : Type u_2} [] [] (b : β) (a : α) :
↑() a = b
def ContinuousMap.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(β, γ)) (g : C(α, β)) :
C(α, γ)

The composition of continuous maps, as a continuous map.

Instances For
@[simp]
theorem ContinuousMap.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(β, γ)) (g : C(α, β)) :
↑() = f g
@[simp]
theorem ContinuousMap.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(β, γ)) (g : C(α, β)) (a : α) :
↑() a = f (g a)
@[simp]
theorem ContinuousMap.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] [] [] [] (f : C(γ, δ)) (g : C(β, γ)) (h : C(α, β)) :
@[simp]
theorem ContinuousMap.id_comp {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) :
@[simp]
theorem ContinuousMap.comp_id {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) :
@[simp]
theorem ContinuousMap.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (c : γ) (f : C(α, β)) :
@[simp]
theorem ContinuousMap.comp_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(β, γ)) (b : β) :
= ContinuousMap.const α (f b)
@[simp]
theorem ContinuousMap.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f₁ : C(β, γ)} {f₂ : C(β, γ)} {g : C(α, β)} (hg : ) :
= f₁ = f₂
@[simp]
theorem ContinuousMap.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : C(β, γ)} {g₁ : C(α, β)} {g₂ : C(α, β)} (hf : ) :
= g₁ = g₂
instance ContinuousMap.instNontrivialContinuousMap {α : Type u_1} {β : Type u_2} [] [] [] [] :
@[simp]
theorem ContinuousMap.fst_apply {α : Type u_1} {β : Type u_2} [] [] :
ContinuousMap.fst = Prod.fst
def ContinuousMap.fst {α : Type u_1} {β : Type u_2} [] [] :
C(α × β, α)

Prod.fst : (x, y) ↦ x as a bundled continuous map.

Instances For
@[simp]
theorem ContinuousMap.snd_apply {α : Type u_1} {β : Type u_2} [] [] :
ContinuousMap.snd = Prod.snd
def ContinuousMap.snd {α : Type u_1} {β : Type u_2} [] [] :
C(α × β, β)

Prod.snd : (x, y) ↦ y as a bundled continuous map.

Instances For
def ContinuousMap.prodMk {α : Type u_1} [] {β₁ : Type u_7} {β₂ : Type u_8} [] [] (f : C(α, β₁)) (g : C(α, β₂)) :
C(α, β₁ × β₂)

Given two continuous maps f and g, this is the continuous map x ↦ (f x, g x).

Instances For
@[simp]
theorem ContinuousMap.prodMap_apply {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [] [] [] [] (f : C(α₁, α₂)) (g : C(β₁, β₂)) :
∀ (a : α₁ × β₁), ↑() a = Prod.map (f) (g) a
def ContinuousMap.prodMap {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [] [] [] [] (f : C(α₁, α₂)) (g : C(β₁, β₂)) :
C(α₁ × β₁, α₂ × β₂)

Given two continuous maps f and g, this is the continuous map (x, y) ↦ (f x, g y).

Instances For
@[simp]
theorem ContinuousMap.prod_eval {α : Type u_1} [] {β₁ : Type u_7} {β₂ : Type u_8} [] [] (f : C(α, β₁)) (g : C(α, β₂)) (a : α) :
↑() a = (f a, g a)
@[simp]
theorem ContinuousMap.prodSwap_apply {α : Type u_1} {β : Type u_2} [] [] (x : α × β) :
ContinuousMap.prodSwap x = (x.snd, x.fst)
def ContinuousMap.prodSwap {α : Type u_1} {β : Type u_2} [] [] :
C(α × β, β × α)

Prod.swap bundled as a ContinuousMap.

Instances For
@[simp]
theorem ContinuousMap.sigmaMk_apply {ι : Type u_5} {Y : ιType u_6} [(i : ι) → TopologicalSpace (Y i)] (i : ι) (snd : Y i) :
↑() snd = { fst := i, snd := snd }
def ContinuousMap.sigmaMk {ι : Type u_5} {Y : ιType u_6} [(i : ι) → TopologicalSpace (Y i)] (i : ι) :
C(Y i, (i : ι) × Y i)

Sigma.mk i as a bundled continuous map.

Instances For
def ContinuousMap.pi {I : Type u_5} {A : Type u_6} {X : IType u_7} [] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)) :
C(A, (i : I) → X i)

Abbreviation for product of continuous maps, which is continuous

Instances For
@[simp]
theorem ContinuousMap.pi_eval {I : Type u_5} {A : Type u_6} {X : IType u_7} [] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)) (a : A) :
↑() a = fun i => ↑(f i) a
@[simp]
theorem ContinuousMap.eval_apply {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] (i : I) :
def ContinuousMap.eval {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] (i : I) :
C((j : I) → X j, X i)

Evaluation at point as a bundled continuous map.

Instances For
@[simp]
theorem ContinuousMap.piMap_apply {I : Type u_5} {X : IType u_7} {Y : IType u_8} [(i : I) → TopologicalSpace (X i)] [(i : I) → TopologicalSpace (Y i)] (f : (i : I) → C(X i, Y i)) (a : (i : I) → X i) (i : I) :
↑() a i = ↑(f i) (a i)
def ContinuousMap.piMap {I : Type u_5} {X : IType u_7} {Y : IType u_8} [(i : I) → TopologicalSpace (X i)] [(i : I) → TopologicalSpace (Y i)] (f : (i : I) → C(X i, Y i)) :
C((i : I) → X i, (i : I) → Y i)

Combine a collection of bundled continuous maps C(X i, Y i) into a bundled continuous map C(∀ i, X i, ∀ i, Y i).

Instances For
def ContinuousMap.restrict {α : Type u_1} {β : Type u_2} [] [] (s : Set α) (f : C(α, β)) :
C(s, β)

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

Instances For
@[simp]
theorem ContinuousMap.coe_restrict {α : Type u_1} {β : Type u_2} [] [] (s : Set α) (f : C(α, β)) :
↑() = f Subtype.val
@[simp]
theorem ContinuousMap.restrict_apply {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (s : Set α) (x : s) :
↑() x = f x
@[simp]
theorem ContinuousMap.restrict_apply_mk {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (s : Set α) (x : α) (hx : x s) :
↑() { val := x, property := hx } = f x
theorem ContinuousMap.injective_restrict {α : Type u_1} {β : Type u_2} [] [] [] {s : Set α} (hs : ) :
@[simp]
theorem ContinuousMap.restrictPreimage_apply {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (s : Set β) :
∀ (a : ↑(f ⁻¹' s)), ↑() a = Set.restrictPreimage s (f) a
def ContinuousMap.restrictPreimage {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (s : Set β) :
C(↑(f ⁻¹' s), s)

The restriction of a continuous map to the preimage of a set.

Instances For
noncomputable def ContinuousMap.liftCover {α : Type u_1} {β : Type u_2} [] [] {ι : Type u_5} (S : ιSet α) (φ : (i : ι) → C(↑(S i), β)) (hφ : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }) (hS : ∀ (x : α), i, S i nhds x) :
C(α, β)

A family φ i of continuous maps C(S i, β), where the domains S i contain a neighbourhood of each point in α and the functions φ i agree pairwise on intersections, can be glued to construct a continuous map in C(α, β).

Instances For
@[simp]
theorem ContinuousMap.liftCover_coe {α : Type u_1} {β : Type u_2} [] [] {ι : Type u_5} {S : ιSet α} {φ : (i : ι) → C(↑(S i), β)} {hφ : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }} {hS : ∀ (x : α), i, S i nhds x} {i : ι} (x : ↑(S i)) :
↑(ContinuousMap.liftCover S φ hS) x = ↑(φ i) x
theorem ContinuousMap.liftCover_restrict {α : Type u_1} {β : Type u_2} [] [] {ι : Type u_5} {S : ιSet α} {φ : (i : ι) → C(↑(S i), β)} {hφ : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }} {hS : ∀ (x : α), i, S i nhds x} {i : ι} :
noncomputable def ContinuousMap.liftCover' {α : Type u_1} {β : Type u_2} [] [] (A : Set (Set α)) (F : (s : Set α) → s AC(s, β)) (hF : ∀ (s : Set α) (hs : s A) (t : Set α) (ht : t A) (x : α) (hxi : x s) (hxj : x t), ↑(F s hs) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }) (hA : ∀ (x : α), i, i A i nhds x) :
C(α, β)

A family F s of continuous maps C(s, β), where (1) the domains s are taken from a set A of sets in α which contain a neighbourhood of each point in α and (2) the functions F s agree pairwise on intersections, can be glued to construct a continuous map in C(α, β).

Instances For
@[simp]
theorem ContinuousMap.liftCover_coe' {α : Type u_1} {β : Type u_2} [] [] {A : Set (Set α)} {F : (s : Set α) → s AC(s, β)} {hF : ∀ (s : Set α) (hs : s A) (t : Set α) (ht : t A) (x : α) (hxi : x s) (hxj : x t), ↑(F s hs) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }} {hA : ∀ (x : α), i, i A i nhds x} {s : Set α} {hs : s A} (x : s) :
↑(ContinuousMap.liftCover' A F hF hA) x = ↑(F s hs) x
@[simp]
theorem ContinuousMap.liftCover_restrict' {α : Type u_1} {β : Type u_2} [] [] {A : Set (Set α)} {F : (s : Set α) → s AC(s, β)} {hF : ∀ (s : Set α) (hs : s A) (t : Set α) (ht : t A) (x : α) (hxi : x s) (hxj : x t), ↑(F s hs) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }} {hA : ∀ (x : α), i, i A i nhds x} {s : Set α} {hs : s A} :
@[simp]
theorem Homeomorph.toContinuousMap_apply {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ₜ β) (a : α) :
= e a
def Homeomorph.toContinuousMap {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ₜ β) :
C(α, β)

The forward direction of a homeomorphism, as a bundled continuous map.

Instances For
instance Homeomorph.instCoeHomeomorphContinuousMap {α : Type u_1} {β : Type u_2} [] [] :
Coe (α ≃ₜ β) C(α, β)

Homeomorph.toContinuousMap as a coercion.

@[simp]
theorem Homeomorph.coe_refl {α : Type u_1} [] :
@[simp]
theorem Homeomorph.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : α ≃ₜ β) (g : β ≃ₜ γ) :
@[simp]
theorem Homeomorph.symm_comp_toContinuousMap {α : Type u_1} {β : Type u_2} [] [] (f : α ≃ₜ β) :

Left inverse to a continuous map from a homeomorphism, mirroring Equiv.symm_comp_self.

@[simp]
theorem Homeomorph.toContinuousMap_comp_symm {α : Type u_1} {β : Type u_2} [] [] (f : α ≃ₜ β) :

Right inverse to a continuous map from a homeomorphism, mirroring Equiv.self_comp_symm.