mathlib3 documentation

topology.continuous_function.basic

Continuous bundled maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) [topological_space α] [topological_space β] :
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)) [topological_space α] [topological_space β] [self : continuous_map_class F α β] :
fun_like F α (λ (_x : α), β)
@[class]
structure continuous_map_class (F : Type u_1) (α : out_param (Type u_2)) (β : out_param (Type u_3)) [topological_space α] [topological_space β] :
Type (max u_1 u_2 u_3)

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} [topological_space α] [topological_space β] [continuous_map_class F α β] (f : F) (a : α) :
theorem map_continuous_within_at {F : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [continuous_map_class F α β] (f : F) (s : set α) (a : α) :
@[protected, instance]
def continuous_map.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [continuous_map_class F α β] :
Equations

Continuous maps #

@[protected, instance]
def continuous_map.has_coe_to_fun {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
has_coe_to_fun C(α, β) (λ (_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} [topological_space α] [topological_space β] {f : C(α, β)} :
@[protected, simp, norm_cast]
theorem continuous_map.coe_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {F : Type u_3} [continuous_map_class F α β] (f : F) :
@[ext]
theorem continuous_map.ext {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : C(α, β)} (h : (a : α), f a = g a) :
f = g
@[protected]
def continuous_map.copy {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (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
@[simp]
theorem continuous_map.coe_copy {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem continuous_map.copy_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]
theorem continuous_map.continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) :

Deprecated. Use map_continuous instead.

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

Deprecated. Use map_continuous_at instead.

@[protected]
theorem continuous_map.congr_fun {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {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} [topological_space α] [topological_space β] (f : C(α, β)) {x y : α} (h : x = y) :
f x = f y

Deprecated. Use fun_like.congr_arg instead.

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

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

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

The identity as a continuous map.

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

The constant map as a continuous map.

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

The composition of continuous maps, as a continuous map.

Equations
Instances for continuous_map.comp
@[simp]
theorem continuous_map.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : C(β, γ)) (g : C(α, β)) :
(f.comp g) = f g
@[simp]
theorem continuous_map.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (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} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] (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} [topological_space α] [topological_space β] (f : C(α, β)) :
@[simp]
theorem continuous_map.comp_id {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) :
@[simp]
theorem continuous_map.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (c : γ) (f : C(α, β)) :
@[simp]
theorem continuous_map.comp_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : C(β, γ)) (b : β) :
theorem continuous_map.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {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} [topological_space α] [topological_space β] [topological_space γ] {f : C(β, γ)} {g₁ g₂ : C(α, β)} (hf : function.injective f) :
f.comp g₁ = f.comp g₂ g₁ = g₂
@[protected, instance]
def continuous_map.prod_mk {α : Type u_1} [topological_space α] {β₁ : Type u_7} {β₂ : Type u_8} [topological_space β₁] [topological_space β₂] (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} [topological_space α₁] [topological_space α₂] [topological_space β₁] [topological_space β₂] (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} [topological_space α₁] [topological_space α₂] [topological_space β₁] [topological_space β₂] (f : C(α₁, α₂)) (g : C(β₁, β₂)) (x : α₁ × β₁) :
@[simp]
theorem continuous_map.prod_eval {α : Type u_1} [topological_space α] {β₁ : Type u_7} {β₂ : Type u_8} [topological_space β₁] [topological_space β₂] (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} [topological_space A] [Π (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} [topological_space A] [Π (i : I), topological_space (X i)] (f : Π (i : I), C(A, X i)) (a : A) :
(continuous_map.pi f) a = λ (i : I), (f i) a
def continuous_map.restrict {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (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} [topological_space α] [topological_space β] (s : set α) (f : C(α, β)) :
@[simp]
theorem continuous_map.restrict_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (s : set α) (x : s) :
@[simp]
theorem continuous_map.restrict_apply_mk {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (s : set α) (x : α) (hx : x s) :
@[simp]
theorem continuous_map.restrict_preimage_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (s : set β) (ᾰ : (f ⁻¹' s)) :
def continuous_map.restrict_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (s : set β) :

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

Equations
noncomputable def continuous_map.lift_cover {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {ι : 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} [topological_space α] [topological_space β] {ι : 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)) :
(continuous_map.lift_cover S φ hS) x = (φ i) x
@[simp]
theorem continuous_map.lift_cover_restrict {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {ι : 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 : ι} :
noncomputable def continuous_map.lift_cover' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (A : set (set α)) (F : Π (s : set α), s A C(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} [topological_space α] [topological_space β] {A : set (set α)} {F : Π (s : set α), s A C(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) :
(continuous_map.lift_cover' A F hF hA) x = (F s hs) x
@[simp]
theorem continuous_map.lift_cover_restrict' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {A : set (set α)} {F : Π (s : set α), s A C(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} :
@[simp]
theorem homeomorph.to_continuous_map_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : α ≃ₜ β) (ᾰ : α) :
def homeomorph.to_continuous_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : α ≃ₜ β) :
C(α, β)

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

Equations
@[simp]
theorem homeomorph.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : α ≃ₜ β) (g : β ≃ₜ γ) :
@[simp]

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

@[simp]

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