# mathlibdocumentation

topology.continuous_function.basic

# Continuous bundled maps #

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

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

structure continuous_map (α : Type u_1) (β : Type u_2)  :
Type (max u_1 u_2)

The type of continuous maps from α to β.

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

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

Instances for continuous_map
@[instance]
def continuous_map_class.to_fun_like (F : Type u_1) (α : out_param (Type u_2)) (β : out_param (Type u_3)) [self : β] :
α (λ (_x : α), β)
@[class]
structure continuous_map_class (F : Type u_1) (α : out_param (Type u_2)) (β : out_param (Type u_3))  :
Type (max u_1 u_2 u_3)
• coe : F → Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_continuous : ∀ (f : F),

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

You should extend this class when you extend continuous_map.

Instances of this typeclass
Instances of other typeclasses for continuous_map_class
• continuous_map_class.has_sizeof_inst
theorem map_continuous_at {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) (a : α) :
theorem map_continuous_within_at {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) (s : set α) (a : α) :
@[protected, instance]
def continuous_map.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] :
C(α, β)
Equations

### Continuous maps #

@[protected, instance]
def continuous_map.continuous_map_class {α : Type u_1} {β : Type u_2}  :
β
Equations
@[protected, instance]
def continuous_map.has_coe_to_fun {α : Type u_1} {β : Type u_2}  :
(λ (_x : C(α, β)), α → β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[simp]
theorem continuous_map.to_fun_eq_coe {α : Type u_1} {β : Type u_2} {f : C(α, β)} :
@[ext]
theorem continuous_map.ext {α : Type u_1} {β : Type u_2} {f g : C(α, β)} (h : ∀ (a : α), f a = g a) :
f = g
@[protected]
def continuous_map.copy {α : Type u_1} {β : Type u_2} (f : C(α, β)) (f' : α → β) (h : f' = f) :
C(α, β)

Copy of a continuous_map with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
theorem continuous_map.continuous {α : Type u_1} {β : Type u_2} (f : C(α, β)) :

Deprecated. Use map_continuous instead.

@[continuity]
theorem continuous_map.continuous_set_coe {α : Type u_1} {β : Type u_2} (s : set C(α, β)) (f : s) :
@[protected]
theorem continuous_map.continuous_at {α : Type u_1} {β : Type u_2} (f : C(α, β)) (x : α) :

Deprecated. Use map_continuous_at instead.

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

Deprecated. Use fun_like.congr_fun instead.

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

Deprecated. Use fun_like.congr_arg instead.

theorem continuous_map.coe_injective {α : Type u_1} {β : Type u_2}  :
@[simp]
theorem continuous_map.coe_mk {α : Type u_1} {β : Type u_2} (f : α → β) (h : continuous f) :
theorem continuous_map.map_specializes {α : Type u_1} {β : Type u_2} (f : C(α, β)) {x y : α} (h : x y) :
f x f y
def continuous_map.equiv_fn_of_discrete (α : Type u_1) (β : Type u_2)  :
C(α, β) (α → β)

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

Equations
@[simp]
theorem continuous_map.equiv_fn_of_discrete_symm_apply_apply (α : Type u_1) (β : Type u_2) (f : α → β) (ᾰ : α) :
( f) = f ᾰ
@[simp]
theorem continuous_map.equiv_fn_of_discrete_apply (α : Type u_1) (β : Type u_2) (f : C(α, β)) (ᾰ : α) :
= f ᾰ
@[protected]
def continuous_map.id (α : Type u_1)  :
C(α, α)

The identity as a continuous map.

Equations
@[simp]
theorem continuous_map.coe_id (α : Type u_1)  :
def continuous_map.const (α : Type u_1) {β : Type u_2} (b : β) :
C(α, β)

The constant map as a continuous map.

Equations
@[simp]
theorem continuous_map.coe_const (α : Type u_1) {β : Type u_2} (b : β) :
b) =
@[protected, instance]
def continuous_map.inhabited (α : Type u_1) {β : Type u_2} [inhabited β] :
Equations
@[simp]
theorem continuous_map.id_apply {α : Type u_1} (a : α) :
a = a
@[simp]
theorem continuous_map.const_apply {α : Type u_1} {β : Type u_2} (b : β) (a : α) :
b) a = b
def continuous_map.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : C(β, γ)) (g : C(α, β)) :
C(α, γ)

The composition of continuous maps, as a continuous map.

Equations
@[simp]
theorem continuous_map.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : C(β, γ)) (g : C(α, β)) :
(f.comp g) = f g
@[simp]
theorem continuous_map.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : C(β, γ)) (g : C(α, β)) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem continuous_map.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : C(γ, δ)) (g : C(β, γ)) (h : C(α, β)) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem continuous_map.id_comp {α : Type u_1} {β : Type u_2} (f : C(α, β)) :
f = f
@[simp]
theorem continuous_map.comp_id {α : Type u_1} {β : Type u_2} (f : C(α, β)) :
f.comp = f
@[simp]
theorem continuous_map.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) (f : C(α, β)) :
c).comp f =
@[simp]
theorem continuous_map.comp_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : C(β, γ)) (b : β) :
f.comp b) = (f b)
theorem continuous_map.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f₁ f₂ : C(β, γ)} {g : C(α, β)} (hg : function.surjective g) :
f₁.comp g = f₂.comp g f₁ = f₂
theorem continuous_map.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : C(β, γ)} {g₁ g₂ : C(α, β)} (hf : function.injective f) :
f.comp g₁ = f.comp g₂ g₁ = g₂
@[protected, instance]
def continuous_map.nontrivial {α : Type u_1} {β : Type u_2} [nonempty α] [nontrivial β] :
def continuous_map.prod_mk {α : 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).

Equations
def continuous_map.prod_map {α₁ : 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).

Equations
@[simp]
theorem continuous_map.prod_map_apply {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} (f : C(α₁, α₂)) (g : C(β₁, β₂)) (x : α₁ × β₁) :
(f.prod_map g) x = g x
@[simp]
theorem continuous_map.prod_eval {α : Type u_1} {β₁ : Type u_7} {β₂ : Type u_8} (f : C(α, β₁)) (g : C(α, β₂)) (a : α) :
(f.prod_mk g) a = (f a, g a)
def continuous_map.pi {I : Type u_5} {A : Type u_6} {X : I → Type u_7} [Π (i : I), topological_space (X i)] (f : Π (i : I), C(A, X i)) :
C(A, Π (i : I), X i)

Abbreviation for product of continuous maps, which is continuous

Equations
@[simp]
theorem continuous_map.pi_eval {I : Type u_5} {A : Type u_6} {X : I → Type u_7} [Π (i : I), topological_space (X i)] (f : Π (i : I), C(A, X i)) (a : A) :
a = λ (i : I), (f i) a
def continuous_map.restrict {α : Type u_1} {β : Type u_2} (s : set α) (f : C(α, β)) :

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

Equations
@[simp]
theorem continuous_map.coe_restrict {α : Type u_1} {β : Type u_2} (s : set α) (f : C(α, β)) :
@[simp]
theorem continuous_map.restrict_preimage_apply {α : Type u_1} {β : Type u_2} (f : C(α, β)) (s : set β) (ᾰ : (f ⁻¹' s)) :
(f.restrict_preimage s) =
def continuous_map.restrict_preimage {α : Type u_1} {β : Type u_2} (f : C(α, β)) (s : set β) :

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

Equations
noncomputable def continuous_map.lift_cover {α : 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) x, hxi⟩ = (φ j) x, 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(α, β).

Equations
@[simp]
theorem continuous_map.lift_cover_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) x, hxi⟩ = (φ j) x, hxj⟩} {hS : ∀ (x : α), ∃ (i : ι), S i nhds x} {i : ι} (x : (S i)) :
hS) x = (φ i) x
@[simp]
theorem continuous_map.lift_cover_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) x, hxi⟩ = (φ j) x, hxj⟩} {hS : ∀ (x : α), ∃ (i : ι), S i nhds x} {i : ι} :
hS) = φ i
noncomputable def continuous_map.lift_cover' {α : 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) x, hxi⟩ = (F t ht) x, hxj⟩) (hA : ∀ (x : α), ∃ (i : set α) (H : 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(α, β).

Equations
@[simp]
theorem continuous_map.lift_cover_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) x, hxi⟩ = (F t ht) x, hxj⟩} {hA : ∀ (x : α), ∃ (i : set α) (H : i A), i nhds x} {s : set α} {hs : s A} (x : s) :
hF hA) x = (F s hs) x
@[simp]
theorem continuous_map.lift_cover_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) x, hxi⟩ = (F t ht) x, hxj⟩} {hA : ∀ (x : α), ∃ (i : set α) (H : i A), i nhds x} {s : set α} {hs : s A} :
hF hA) = F s hs
@[simp]
theorem homeomorph.to_continuous_map_apply {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) (ᾰ : α) :
def homeomorph.to_continuous_map {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) :
C(α, β)

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

Equations
@[protected, instance]
def homeomorph.continuous_map.has_coe {α : Type u_1} {β : Type u_2}  :
has_coe ≃ₜ β) C(α, β)

homeomorph.to_continuous_map as a coercion.

Equations
theorem homeomorph.to_continuous_map_as_coe {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β) :
@[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_to_continuous_map {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β) :

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

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

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