# mathlibdocumentation

topology.continuous_function.basic

# 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)

Bundled continuous maps.

@[instance]
def continuous_map.has_coe_to_fun {α : Type u_1} {β : Type u_2}  :
Equations
@[simp]
theorem continuous_map.to_fun_eq_coe {α : Type u_1} {β : Type u_2} {f : C(α, β)} :
theorem continuous_map.continuous {α : Type u_1} {β : Type u_2} (f : C(α, β)) :
theorem continuous_map.continuous_set_coe {α : Type u_1} {β : Type u_2} (s : set C(α, β)) (f : s) :
theorem continuous_map.continuous_at {α : Type u_1} {β : Type u_2} (f : C(α, β)) (x : α) :
theorem continuous_map.continuous_within_at {α : Type u_1} {β : Type u_2} (f : C(α, β)) (s : set α) (x : α) :
theorem continuous_map.congr_fun {α : Type u_1} {β : Type u_2} {f g : C(α, β)} (H : f = g) (x : α) :
f x = g x
theorem continuous_map.congr_arg {α : Type u_1} {β : Type u_2} (f : C(α, β)) {x y : α} (h : x = y) :
f x = f y
@[ext]
theorem continuous_map.ext {α : Type u_1} {β : Type u_2} {f g : C(α, β)} (H : ∀ (x : α), f x = g x) :
f = g
theorem continuous_map.ext_iff {α : Type u_1} {β : Type u_2} {f g : C(α, β)} :
f = g ∀ (x : α), f x = g x
@[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(α, β) (h : f = g) :
f = g
@[simp]
theorem continuous_map.coe_mk {α : Type u_1} {β : Type u_2} (f : α → β) (h : continuous f) :
def continuous_map.equiv_fn_of_discrete (α : Type u_1) (β : Type u_2)  :
C(α, β) (α → β)

The continuous functions from α to β are the same as the plain functions when α is discrete.

Equations
@[simp]
theorem continuous_map.equiv_fn_of_discrete_apply (α : Type u_1) (β : Type u_2) (f : C(α, β)) (ᾰ : α) :
= f ᾰ
@[simp]
theorem continuous_map.equiv_fn_of_discrete_symm_apply_to_fun (α : Type u_1) (β : Type u_2) (f : α → β) (ᾰ : α) :
( f) = f ᾰ
def continuous_map.id {α : Type u_1}  :
C(α, α)

The identity as a continuous map.

Equations
@[simp]
theorem continuous_map.id_coe {α : Type u_1}  :
theorem continuous_map.id_apply {α : Type u_1} (a : α) :
def continuous_map.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : C(β, γ)) (g : C(α, β)) :
C(α, γ)

The composition of continuous maps, as a continuous map.

Equations
@[simp]
theorem continuous_map.comp_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : C(β, γ)) (g : C(α, β)) :
(f.comp g) = f g
theorem continuous_map.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : C(β, γ)) (g : C(α, β)) (a : α) :
(f.comp g) a = f (g a)
def continuous_map.const {α : Type u_1} {β : Type u_2} (b : β) :
C(α, β)

Constant map as a continuous map

Equations
@[simp]
theorem continuous_map.const_coe {α : Type u_1} {β : Type u_2} (b : β) :
= λ (x : α), b
theorem continuous_map.const_apply {α : Type u_1} {β : Type u_2} (b : β) (a : α) :
= b
@[instance]
def continuous_map.nontrivial {α : Type u_1} {β : Type u_2} [nonempty α] [nontrivial β] :
def continuous_map.abs {α : Type u_1} {β : Type u_2} (f : C(α, β)) :
C(α, β)

The pointwise absolute value of a continuous function as a continuous function.

Equations
@[instance]
def continuous_map.has_abs {α : Type u_1} {β : Type u_2}  :
Equations
@[simp]
theorem continuous_map.abs_apply {α : Type u_1} {β : Type u_2} (f : C(α, β)) (x : α) :
|f| x = |f x|

We now set up the partial order and lattice structure (given by pointwise min and max) on continuous functions.

@[instance]
def continuous_map.partial_order {α : Type u_1} {β : Type u_2}  :
Equations
theorem continuous_map.le_def {α : Type u_1} {β : Type u_2} {f g : C(α, β)} :
f g ∀ (a : α), f a g a
theorem continuous_map.lt_def {α : Type u_1} {β : Type u_2} {f g : C(α, β)} :
f < g (∀ (a : α), f a g a) ∃ (a : α), f a < g a
@[instance]
def continuous_map.has_sup {α : Type u_1} {β : Type u_2} [linear_order β]  :
Equations
@[simp]
theorem continuous_map.sup_coe {α : Type u_1} {β : Type u_2} [linear_order β] (f g : C(α, β)) :
(f g) = f g
@[simp]
theorem continuous_map.sup_apply {α : Type u_1} {β : Type u_2} [linear_order β] (f g : C(α, β)) (a : α) :
(f g) a = max (f a) (g a)
@[instance]
def continuous_map.semilattice_sup {α : Type u_1} {β : Type u_2} [linear_order β]  :
Equations
@[instance]
def continuous_map.has_inf {α : Type u_1} {β : Type u_2} [linear_order β]  :
Equations
@[simp]
theorem continuous_map.inf_coe {α : Type u_1} {β : Type u_2} [linear_order β] (f g : C(α, β)) :
(f g) = f g
@[simp]
theorem continuous_map.inf_apply {α : Type u_1} {β : Type u_2} [linear_order β] (f g : C(α, β)) (a : α) :
(f g) a = min (f a) (g a)
@[instance]
def continuous_map.semilattice_inf {α : Type u_1} {β : Type u_2} [linear_order β]  :
Equations
@[instance]
def continuous_map.lattice {α : Type u_1} {β : Type u_2} [linear_order β]  :
Equations
theorem continuous_map.sup'_apply {β : Type u_2} {γ : Type u_3} [linear_order γ] {ι : Type u_1} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) (b : β) :
(s.sup' H f) b = s.sup' H (λ (a : ι), (f a) b)
@[simp]
theorem continuous_map.sup'_coe {β : Type u_2} {γ : Type u_3} [linear_order γ] {ι : Type u_1} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) :
(s.sup' H f) = s.sup' H (λ (a : ι), (f a))
theorem continuous_map.inf'_apply {β : Type u_2} {γ : Type u_3} [linear_order γ] {ι : Type u_1} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) (b : β) :
(s.inf' H f) b = s.inf' H (λ (a : ι), (f a) b)
@[simp]
theorem continuous_map.inf'_coe {β : Type u_2} {γ : Type u_3} [linear_order γ] {ι : Type u_1} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) :
(s.inf' H f) = s.inf' H (λ (a : ι), (f a))
def continuous_map.restrict {α : Type u_1} {β : Type u_2} (s : set α) (f : C(α, β)) :

The restriction of a continuous function α → β to a subset s of α.

Equations
@[simp]
theorem continuous_map.coe_restrict {α : Type u_1} {β : Type u_2} (s : set α) (f : C(α, β)) :
def continuous_map.Icc_extend {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) (f : C((set.Icc a b), β)) :
C(α, β)

Extend a continuous function f : C(set.Icc a b, β) to a function f : C(α, β).

Equations
@[simp]
theorem continuous_map.coe_Icc_extend {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) (f : C((set.Icc a b), β)) :
def continuous_map.lift_cover {α : Type u_1} {β : Type u_2} {ι : 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) :
C(α, β)

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
@[simp]
theorem continuous_map.lift_cover_coe {α : Type u_1} {β : Type u_2} {ι : 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)) :
hS) x = (φ i) x
@[simp]
theorem continuous_map.lift_cover_restrict {α : Type u_1} {β : Type u_2} {ι : 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 : ι} :
hS) = φ i
def continuous_map.lift_cover' {α : Type u_1} {β : Type u_2} (A : set (set α)) (F : Π (s : set α), s AC(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) :
C(α, β)

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(α, β).

Equations
@[simp]
theorem continuous_map.lift_cover_coe' {α : Type u_1} {β : Type u_2} {A : set (set α)} {F : Π (s : set α), s AC(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) :
hF hA) x = (F s hs) x
@[simp]
theorem continuous_map.lift_cover_restrict' {α : Type u_1} {β : Type u_2} {A : set (set α)} {F : Π (s : set α), s AC(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} :
hF hA) = F s hs
def homeomorph.to_continuous_map {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) :
C(α, β)

The forward direction of a homeomorphism, as a bundled continuous map.

Equations
@[simp]
theorem homeomorph.to_continuous_map_to_fun {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) (ᾰ : α) :