mathlib documentation

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

The identity as a continuous map.

Equations
@[simp]
theorem continuous_map.id_apply {α : Type u_1} [topological_space α] (a : α) :
def continuous_map.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (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} [topological_space α] [topological_space β] [topological_space γ] (f : C(β, γ)) (g : C(α, β)) :
(f.comp g) = f g
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 : α) :
(f.comp g) a = f (g a)
def continuous_map.const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (b : β) :
C(α, β)

Constant map as a continuous map

Equations
@[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 : α) :
@[instance]
def continuous_map.nontrivial {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [nonempty α] [nontrivial β] :
def continuous_map.abs {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_ordered_add_comm_group β] [order_topology β] (f : C(α, β)) :
C(α, β)

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

Equations
@[simp]
theorem continuous_map.abs_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_ordered_add_comm_group β] [order_topology β] (f : C(α, β)) (x : α) :
(f.abs) x = abs (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} [topological_space α] [topological_space β] [partial_order β] :
Equations
theorem continuous_map.le_def {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [partial_order β] {f g : C(α, β)} :
f g ∀ (a : α), f a g a
theorem continuous_map.lt_def {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [partial_order β] {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} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] :
Equations
@[simp]
theorem continuous_map.sup_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] (f g : C(α, β)) :
(f g) = f g
@[simp]
theorem continuous_map.sup_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] (f g : C(α, β)) (a : α) :
(f g) a = max (f a) (g a)
@[instance]
def continuous_map.has_inf {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] :
Equations
@[simp]
theorem continuous_map.inf_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] (f g : C(α, β)) :
(f g) = f g
@[simp]
theorem continuous_map.inf_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] (f g : C(α, β)) (a : α) :
(f g) a = min (f a) (g a)
theorem continuous_map.sup'_apply {β : Type u_2} {γ : Type u_3} [topological_space β] [topological_space γ] [linear_order γ] [order_closed_topology γ] {ι : 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} [topological_space β] [topological_space γ] [linear_order γ] [order_closed_topology γ] {ι : 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} [topological_space β] [topological_space γ] [linear_order γ] [order_closed_topology γ] {ι : 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} [topological_space β] [topological_space γ] [linear_order γ] [order_closed_topology γ] {ι : Type u_1} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) :
(s.inf' H f) = s.inf' H (λ (a : ι), (f a))
def homeomorph.to_continuous_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (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} [topological_space α] [topological_space β] (e : α ≃ₜ β) (ᾰ : α) :