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 c.to_fun . "continuity'"
Bundled continuous maps.
@[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 = {F := λ (x : C(α, β)), α → β, coe := continuous_map.to_fun _inst_2}
theorem
continuous_map.coe_continuous
{α : 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 : ∀ (x : α), ⇑f x = ⇑g x) :
f = g
@[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
The identity as a continuous map.
Equations
- continuous_map.id = {to_fun := id α, continuous_to_fun := _}
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.
theorem
continuous_map.continuous
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : C(α, β)) :
def
continuous_map.const
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(b : β) :
Takes b in input and gives the continuous bundled function constantly valued b in output.
Equations
- continuous_map.const b = {to_fun := λ (x : α), b, continuous_to_fun := _}