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)
[topological_space α]
[topological_space β] :
Type (max u_1 u_2)
- to_fun : α → β
- continuous_to_fun : continuous self.to_fun . "continuity'"
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.
@[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)
- to_fun_like : fun_like F α (λ (_x : α), β)
- map_continuous : ∀ (f : F), continuous ⇑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
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 : α) :
continuous_at ⇑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 : α) :
continuous_within_at ⇑f s 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_map.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, continuous_to_fun := _}}
Continuous maps #
@[protected, instance]
def
continuous_map.continuous_map_class
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
continuous_map_class C(α, β) α β
Equations
- continuous_map.continuous_map_class = {to_fun_like := {coe := continuous_map.to_fun _inst_2, coe_injective' := _}, map_continuous := _}
@[protected, instance]
def
continuous_map.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
@[simp]
theorem
continuous_map.to_fun_eq_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : C(α, β)} :
@[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) :
Copy of a continuous_map with a new to_fun equal to the old one. Useful to fix definitional
equalities.
Equations
- f.copy f' h = {to_fun := f', continuous_to_fun := _}
@[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 : α) :
continuous_at ⇑f 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 : α) :
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) :
Deprecated. Use fun_like.congr_arg instead.
@[protected, instance]
def
continuous_map.inhabited
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[inhabited β] :
Equations
- continuous_map.inhabited = {default := {to_fun := λ (_x : α), default, continuous_to_fun := _}}
theorem
continuous_map.coe_injective
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
@[simp]
theorem
continuous_map.coe_mk
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α → β)
(h : continuous f) :
⇑{to_fun := f, continuous_to_fun := h} = f
def
continuous_map.equiv_fn_of_discrete
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[discrete_topology α] :
The continuous functions from α to β are the same as the plain functions when α is discrete.
@[simp]
theorem
continuous_map.equiv_fn_of_discrete_apply
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[discrete_topology α]
(f : C(α, β))
(ᾰ : α) :
⇑(continuous_map.equiv_fn_of_discrete α β) f ᾰ = ⇑f ᾰ
@[simp]
theorem
continuous_map.equiv_fn_of_discrete_symm_apply_to_fun
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[discrete_topology α]
(f : α → β)
(ᾰ : α) :
⇑(⇑((continuous_map.equiv_fn_of_discrete α β).symm) f) ᾰ = f ᾰ
@[protected]
The identity as a continuous map.
Equations
- continuous_map.id α = {to_fun := id α, continuous_to_fun := _}
@[simp]
def
continuous_map.const
(α : Type u_1)
{β : Type u_2}
[topological_space α]
[topological_space β]
(b : β) :
The constant map as a continuous map.
Equations
- continuous_map.const α b = {to_fun := function.const α b, continuous_to_fun := _}
@[simp]
theorem
continuous_map.coe_const
(α : Type u_1)
{β : Type u_2}
[topological_space α]
[topological_space β]
(b : β) :
⇑(continuous_map.const α b) = function.const α b
@[simp]
theorem
continuous_map.id_apply
{α : Type u_1}
[topological_space α]
(a : α) :
⇑(continuous_map.id α) a = a
@[simp]
theorem
continuous_map.const_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(b : β)
(a : α) :
⇑(continuous_map.const α b) a = b
def
continuous_map.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(f : C(β, γ))
(g : C(α, β)) :
The composition of continuous maps, as a continuous map.
@[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(α, β)) :
@[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 : α) :
@[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(α, β)) :
@[simp]
theorem
continuous_map.id_comp
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : C(α, β)) :
(continuous_map.id β).comp f = f
@[simp]
theorem
continuous_map.comp_id
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : C(α, β)) :
f.comp (continuous_map.id α) = f
@[simp]
theorem
continuous_map.const_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(c : γ)
(f : C(α, β)) :
(continuous_map.const β c).comp f = continuous_map.const α 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 : β) :
f.comp (continuous_map.const α b) = continuous_map.const α (⇑f 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) :
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) :
@[protected, instance]
def
continuous_map.nontrivial
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[nonempty α]
[nontrivial β] :
nontrivial C(α, β)
def
continuous_map.prod_mk
{α : Type u_1}
[topological_space α]
{β₁ : Type u_7}
{β₂ : Type u_8}
[topological_space β₁]
[topological_space β₂]
(f : C(α, β₁))
(g : C(α, β₂)) :
Given two continuous maps f and g, this is the continuous map x ↦ (f x, g x).
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(β₁, β₂)) :
Given two continuous maps f and g, this is the continuous map (x, y) ↦ (f x, g y).
@[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 : α) :
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)) :
Abbreviation for product of continuous maps, which is continuous
Equations
- continuous_map.pi f = {to_fun := λ (a : A) (i : I), ⇑(f i) a, continuous_to_fun := _}
@[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
- continuous_map.restrict s f = {to_fun := ⇑f ∘ coe, continuous_to_fun := _}
@[simp]
theorem
continuous_map.coe_restrict
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(s : set α)
(f : C(α, β)) :
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 ∈ 𝓝 x) :
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
- continuous_map.lift_cover S φ hφ hS = {to_fun := set.lift_cover S (λ (i : ι), ⇑(φ i)) hφ _, continuous_to_fun := _}
@[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 ∈ 𝓝 x}
{i : ι}
(x : ↥(S i)) :
⇑(continuous_map.lift_cover S φ hφ 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 ∈ 𝓝 x}
{i : ι} :
continuous_map.restrict (S i) (continuous_map.lift_cover S φ hφ hS) = φ 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 ∈ 𝓝 x) :
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(α, β).
@[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 ∈ 𝓝 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 ∈ 𝓝 x}
{s : set α}
{hs : s ∈ A} :
continuous_map.restrict s (continuous_map.lift_cover' A F hF hA) = F s hs
def
homeomorph.to_continuous_map
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β) :
The forward direction of a homeomorphism, as a bundled continuous map.
Equations
- e.to_continuous_map = {to_fun := ⇑e, continuous_to_fun := _}
@[simp]
theorem
homeomorph.to_continuous_map_to_fun
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β)
(ᾰ : α) :
⇑(e.to_continuous_map) ᾰ = ⇑e ᾰ