# mathlibdocumentation

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)  :
Type (max u_1 u_2)
• to_fun : α → β
• continuous_to_fun : . "continuity'"

Bundled continuous maps.

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

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

theorem continuous_map.coe_continuous {α : Type u_1} {β : Type u_2} {f : C(α, β)} :

@[ext]
theorem continuous_map.ext {α : Type u_1} {β : Type u_2} {f g : C(α, β)} :
(∀ (x : α), f x = g x)f = g

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

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

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

The identity as a continuous map.

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

The composition of continuous maps, as a continuous map.

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

Constant map as a continuous map

Equations