mathlib documentation

topology.continuous_map

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)

Bundled continuous maps.

@[instance]
def continuous_map.has_coe_to_fun {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

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

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(α, β)} :
(∀ (x : α), f x = g x)f = g

@[instance]
def continuous_map.inhabited {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [inhabited β] :

Equations
theorem continuous_map.coe_inj {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] ⦃f g : C(α, β) :
f = gf = g

def continuous_map.id {α : Type u_1} [topological_space α] :
C(α, α)

The identity as a continuous map.

Equations
def continuous_map.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] :
C(β, γ)C(α, β)C(α, γ)

The composition of continuous maps, as a continuous map.

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

Constant map as a continuous map

Equations