# mathlib3documentation

topology.continuous_function.compact

# Continuous functions on a compact space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Continuous functions C(α, β) from a compact space α to a metric space β are automatically bounded, and so acquire various structures inherited from α →ᵇ β.

This file transfers these structures, and restates some lemmas characterising these structures.

If you need a lemma which is proved about α →ᵇ β but not for C(α, β) when α is compact, you should restate it here. You can also use bounded_continuous_function.equiv_continuous_map_of_compact to move functions back and forth.

@[simp]
@[simp]

When α is compact, the bounded continuous maps α →ᵇ β are equivalent to C(α, β).

Equations
@[simp]
noncomputable def continuous_map.add_equiv_bounded_of_compact (α : Type u_1) (β : Type u_2) [metric_space β] [add_monoid β]  :

When α is compact, the bounded continuous maps α →ᵇ 𝕜 are additively equivalent to C(α, 𝕜).

Equations
@[protected, instance]
noncomputable def continuous_map.metric_space (α : Type u_1) (β : Type u_2) [metric_space β] :
Equations

When α is compact, and β is a metric space, the bounded continuous maps α →ᵇ β are isometric to C(α, β).

Equations
@[simp]
@[simp]
@[simp]
theorem bounded_continuous_function.dist_mk_of_compact {α : Type u_1} {β : Type u_2} [metric_space β] (f g : C(α, β)) :
@[simp]
theorem bounded_continuous_function.dist_to_continuous_map {α : Type u_1} {β : Type u_2} [metric_space β] (f g : β) :
theorem continuous_map.dist_apply_le_dist {α : Type u_1} {β : Type u_2} [metric_space β] {f g : C(α, β)} (x : α) :

The pointwise distance is controlled by the distance between functions, by definition.

theorem continuous_map.dist_le {α : Type u_1} {β : Type u_2} [metric_space β] {f g : C(α, β)} {C : } (C0 : 0 C) :
C (x : α), has_dist.dist (f x) (g x) C

The distance between two functions is controlled by the supremum of the pointwise distances

theorem continuous_map.dist_le_iff_of_nonempty {α : Type u_1} {β : Type u_2} [metric_space β] {f g : C(α, β)} {C : } [nonempty α] :
C (x : α), has_dist.dist (f x) (g x) C
theorem continuous_map.dist_lt_iff_of_nonempty {α : Type u_1} {β : Type u_2} [metric_space β] {f g : C(α, β)} {C : } [nonempty α] :
< C (x : α), has_dist.dist (f x) (g x) < C
theorem continuous_map.dist_lt_of_nonempty {α : Type u_1} {β : Type u_2} [metric_space β] {f g : C(α, β)} {C : } [nonempty α] (w : (x : α), has_dist.dist (f x) (g x) < C) :
< C
theorem continuous_map.dist_lt_iff {α : Type u_1} {β : Type u_2} [metric_space β] {f g : C(α, β)} {C : } (C0 : 0 < C) :
< C (x : α), has_dist.dist (f x) (g x) < C
@[protected, instance]
def continuous_map.complete_space {α : Type u_1} {β : Type u_2} [metric_space β]  :
@[continuity]
theorem continuous_map.continuous_eval {α : Type u_1} {β : Type u_2} [metric_space β] :
continuous (λ (p : C(α, β) × α), (p.fst) p.snd)

See also continuous_map.continuous_eval'

@[continuity]
theorem continuous_map.continuous_eval_const {α : Type u_1} {β : Type u_2} [metric_space β] (x : α) :
continuous (λ (f : C(α, β)), f x)

See also continuous_map.continuous_eval_const

theorem continuous_map.continuous_coe {α : Type u_1} {β : Type u_2} [metric_space β] :

See also continuous_map.continuous_coe'

@[protected, instance]
noncomputable def continuous_map.has_norm {α : Type u_1} {E : Type u_3}  :
Equations
@[simp]
theorem bounded_continuous_function.norm_mk_of_compact {α : Type u_1} {E : Type u_3} (f : C(α, E)) :
@[simp]
theorem bounded_continuous_function.norm_to_continuous_map_eq {α : Type u_1} {E : Type u_3} (f : E) :
@[protected, instance]
noncomputable def continuous_map.normed_add_comm_group {α : Type u_1} {E : Type u_3}  :
Equations
@[protected, instance]
def continuous_map.norm_one_class {α : Type u_1} {E : Type u_3} [nonempty α] [has_one E]  :
theorem continuous_map.norm_coe_le_norm {α : Type u_1} {E : Type u_3} (f : C(α, E)) (x : α) :
theorem continuous_map.dist_le_two_norm {α : Type u_1} {E : Type u_3} (f : C(α, E)) (x y : α) :

Distance between the images of any two points is at most twice the norm of the function.

theorem continuous_map.norm_le {α : Type u_1} {E : Type u_3} (f : C(α, E)) {C : } (C0 : 0 C) :
f C (x : α), f x C

The norm of a function is controlled by the supremum of the pointwise norms

theorem continuous_map.norm_le_of_nonempty {α : Type u_1} {E : Type u_3} (f : C(α, E)) [nonempty α] {M : } :
f M (x : α), f x M
theorem continuous_map.norm_lt_iff {α : Type u_1} {E : Type u_3} (f : C(α, E)) {M : } (M0 : 0 < M) :
f < M (x : α), f x < M
theorem continuous_map.nnnorm_lt_iff {α : Type u_1} {E : Type u_3} (f : C(α, E)) {M : nnreal} (M0 : 0 < M) :
f‖₊ < M (x : α), f x‖₊ < M
theorem continuous_map.norm_lt_iff_of_nonempty {α : Type u_1} {E : Type u_3} (f : C(α, E)) [nonempty α] {M : } :
f < M (x : α), f x < M
theorem continuous_map.nnnorm_lt_iff_of_nonempty {α : Type u_1} {E : Type u_3} (f : C(α, E)) [nonempty α] {M : nnreal} :
f‖₊ < M (x : α), f x‖₊ < M
theorem continuous_map.apply_le_norm {α : Type u_1} (f : C(α, )) (x : α) :
theorem continuous_map.neg_norm_le_apply {α : Type u_1} (f : C(α, )) (x : α) :
theorem continuous_map.norm_eq_supr_norm {α : Type u_1} {E : Type u_3} (f : C(α, E)) :
f = (x : α), f x
theorem continuous_map.norm_restrict_mono_set {E : Type u_3} {X : Type u_1} (f : C(X, E)) {K L : topological_space.compacts X} (hKL : K L) :
@[protected, instance]
noncomputable def continuous_map.normed_ring {α : Type u_1} {R : Type u_4} [normed_ring R] :
Equations
@[protected, instance]
def continuous_map.normed_space {α : Type u_1} {E : Type u_3} {𝕜 : Type u_4} [normed_field 𝕜] [ E] :
C(α, E)
Equations
noncomputable def continuous_map.linear_isometry_bounded_of_compact (α : Type u_1) (E : Type u_3) (𝕜 : Type u_4) [normed_field 𝕜] [ E] :

When α is compact and 𝕜 is a normed field, the 𝕜-algebra of bounded continuous maps α →ᵇ β is 𝕜-linearly isometric to C(α, β).

Equations
noncomputable def continuous_map.eval_clm {α : Type u_1} {E : Type u_3} (𝕜 : Type u_4) [normed_field 𝕜] [ E] (x : α) :
C(α, E) →L[𝕜] E

The evaluation at a point, as a continuous linear map from C(α, 𝕜) to 𝕜.

Equations
@[simp]
theorem continuous_map.linear_isometry_bounded_of_compact_symm_apply {α : Type u_1} {E : Type u_3} {𝕜 : Type u_4} [normed_field 𝕜] [ E] (f : E) :
@[simp]
theorem continuous_map.linear_isometry_bounded_of_compact_apply_apply {α : Type u_1} {E : Type u_3} {𝕜 : Type u_4} [normed_field 𝕜] [ E] (f : C(α, E)) (a : α) :
a = f a
@[simp]
theorem continuous_map.linear_isometry_bounded_of_compact_to_isometry_equiv {α : Type u_1} {E : Type u_3} {𝕜 : Type u_4} [normed_field 𝕜] [ E] :
@[simp]
theorem continuous_map.linear_isometry_bounded_of_compact_to_add_equiv {α : Type u_1} {E : Type u_3} {𝕜 : Type u_4} [normed_field 𝕜] [ E] :
@[simp]
theorem continuous_map.linear_isometry_bounded_of_compact_of_compact_to_equiv {α : Type u_1} {E : Type u_3} {𝕜 : Type u_4} [normed_field 𝕜] [ E] :
@[protected, instance]
def continuous_map.normed_algebra {α : Type u_1} {𝕜 : Type u_4} {γ : Type u_5} [normed_field 𝕜] [normed_ring γ] [ γ] :
C(α, γ)
Equations

We now set up some declarations making it convenient to use uniform continuity.

theorem continuous_map.uniform_continuity {α : Type u_1} {β : Type u_2} [metric_space α] [metric_space β] (f : C(α, β)) (ε : ) (h : 0 < ε) :
(δ : ) (H : δ > 0), {x y : α}, < δ has_dist.dist (f x) (f y) < ε
noncomputable def continuous_map.modulus {α : Type u_1} {β : Type u_2} [metric_space α] [metric_space β] (f : C(α, β)) (ε : ) (h : 0 < ε) :

An arbitrarily chosen modulus of uniform continuity for a given function f and ε > 0.

Equations
theorem continuous_map.modulus_pos {α : Type u_1} {β : Type u_2} [metric_space α] [metric_space β] (f : C(α, β)) {ε : } {h : 0 < ε} :
0 < f.modulus ε h
theorem continuous_map.dist_lt_of_dist_lt_modulus {α : Type u_1} {β : Type u_2} [metric_space α] [metric_space β] (f : C(α, β)) (ε : ) (h : 0 < ε) {a b : α} (w : < f.modulus ε h) :
has_dist.dist (f a) (f b) < ε
@[protected]
noncomputable def continuous_linear_map.comp_left_continuous_compact (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] (g : β →L[𝕜] γ) :
C(X, β) →L[𝕜] C(X, γ)

Postcomposition of continuous functions into a normed module by a continuous linear map is a continuous linear map. Transferred version of continuous_linear_map.comp_left_continuous_bounded, upgraded version of continuous_linear_map.comp_left_continuous, similar to linear_map.comp_left.

Equations
@[simp]
theorem continuous_linear_map.to_linear_comp_left_continuous_compact (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] (g : β →L[𝕜] γ) :
@[simp]
theorem continuous_linear_map.comp_left_continuous_compact_apply (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] (g : β →L[𝕜] γ) (f : C(X, β)) (x : X) :
= g (f x)

We now setup variations on comp_right_* f, where f : C(X, Y) (that is, precomposition by a continuous map), as a morphism C(Y, T) → C(X, T), respecting various types of structure.

In particular:

• comp_right_continuous_map, the bundled continuous map (for this we need X Y compact).
• comp_right_homeomorph, when we precompose by a homeomorphism.
• comp_right_alg_hom, when T = R is a topological ring.
def continuous_map.comp_right_continuous_map {X : Type u_1} {Y : Type u_2} (T : Type u_3) [metric_space T] (f : C(X, Y)) :

Precomposition by a continuous map is itself a continuous map between spaces of continuous maps.

Equations
@[simp]
theorem continuous_map.comp_right_continuous_map_apply {X : Type u_1} {Y : Type u_2} (T : Type u_3) [metric_space T] (f : C(X, Y)) (g : C(Y, T)) :
= g.comp f
def continuous_map.comp_right_homeomorph {X : Type u_1} {Y : Type u_2} (T : Type u_3) [metric_space T] (f : X ≃ₜ Y) :

Precomposition by a homeomorphism is itself a homeomorphism between spaces of continuous maps.

Equations
theorem continuous_map.comp_right_alg_hom_continuous {X : Type u_1} {Y : Type u_2} (R : Type u_3) (A : Type u_4) [semiring A] [metric_space A] [ A] (f : C(X, Y)) :

### Local normal convergence #

A sum of continuous functions (on a locally compact space) is "locally normally convergent" if the sum of its sup-norms on any compact subset is summable. This implies convergence in the topology of C(X, E) (i.e. locally uniform convergence).

theorem continuous_map.summable_of_locally_summable_norm {X : Type u_1} [t2_space X] {E : Type u_2} {ι : Type u_3} {F : ι C(X, E)} (hF : (K : , summable (λ (i : ι), (F i))) :

### Star structures #

In this section, if β is a normed ⋆-group, then so is the space of continuous functions from α to β, by using the star operation pointwise.

Furthermore, if α is compact and β is a C⋆-ring, then C(α, β) is a C⋆-ring.

theorem bounded_continuous_function.mk_of_compact_star {α : Type u_1} {β : Type u_2} (f : C(α, β)) :
@[protected, instance]
def continuous_map.normed_star_group {α : Type u_1} {β : Type u_2}  :
@[protected, instance]
def continuous_map.cstar_ring {α : Type u_1} {β : Type u_2} [normed_ring β] [star_ring β] [cstar_ring β] :