Continuous bundled map #
In this file we define the type continuous_map of continuous bundled maps.
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'"
Bundled continuous maps.
@[protected, instance]
def
continuous_map.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
Equations
- continuous_map.has_coe_to_fun = {coe := continuous_map.to_fun _inst_2}
@[simp]
theorem
continuous_map.to_fun_eq_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : C(α, β)} :
@[protected, continuity]
theorem
continuous_map.continuous
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : C(α, β)) :
@[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
@[protected]
theorem
continuous_map.continuous_within_at
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : C(α, β))
(s : set α)
(x : α) :
continuous_within_at ⇑f s x
@[protected]
theorem
continuous_map.congr_fun
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f g : C(α, β)}
(H : f = g)
(x : α) :
@[protected]
theorem
continuous_map.congr_arg
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : C(α, β))
{x y : α}
(h : x = y) :
@[ext]
theorem
continuous_map.ext
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f g : C(α, β)}
(H : ∀ (x : α), ⇑f x = ⇑g x) :
f = g
theorem
continuous_map.ext_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f g : C(α, β)} :
@[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_inj
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
⦃f g : C(α, β)⦄
(h : ⇑f = ⇑g) :
f = g
@[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 ᾰ
The identity as a continuous map.
Equations
- continuous_map.id = {to_fun := id α, continuous_to_fun := _}
@[simp]
theorem
continuous_map.id_apply
{α : Type u_1}
[topological_space α]
(a : α) :
⇑continuous_map.id a = a
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.comp_coe
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(f : C(β, γ))
(g : C(α, β)) :
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.id_comp
{β : Type u_2}
{γ : Type u_3}
[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
def
continuous_map.const
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(b : β) :
Constant map as a continuous map
Equations
- continuous_map.const b = {to_fun := λ (x : α), b, continuous_to_fun := _}
@[simp]
theorem
continuous_map.const_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(b : β) :
⇑(continuous_map.const b) = λ (x : α), b
theorem
continuous_map.const_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(b : β)
(a : α) :
⇑(continuous_map.const b) a = b
@[protected, instance]
def
continuous_map.nontrivial
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[h : nonempty α]
[nontrivial β] :
nontrivial C(α, β)
def
continuous_map.prod_mk
{α : Type u_1}
[topological_space α]
{β₁ : Type u_6}
{β₂ : Type u_7}
[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_4}
{α₂ : Type u_5}
{β₁ : Type u_6}
{β₂ : Type u_7}
[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_6}
{β₂ : Type u_7}
[topological_space β₁]
[topological_space β₂]
(f : C(α, β₁))
(g : C(α, β₂))
(a : α) :
def
continuous_map.pi
{I : Type u_4}
{A : Type u_5}
{X : I → Type u_6}
[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_4}
{A : Type u_5}
{X : I → Type u_6}
[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_4}
(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_4}
{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_4}
{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 ᾰ