Documentation

Mathlib.Topology.ContinuousFunction.Compact

Continuous functions on a compact space #

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 ContinuousMap.equivBoundedOfCompact to move functions back and forth.

@[simp]

theorem ContinuousMap.equivBoundedOfCompact_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :

⇑(ContinuousMap.equivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact

@[simp]

theorem ContinuousMap.equivBoundedOfCompact_symm_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :

⇑(ContinuousMap.equivBoundedOfCompact α β).symm = BoundedContinuousFunction.toContinuousMap

def ContinuousMap.equivBoundedOfCompact (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :

C(α, β) ≃ BoundedContinuousFunction α β

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

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem ContinuousMap.uniformInducing_equivBoundedOfCompact (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :

UniformInducing ⇑(ContinuousMap.equivBoundedOfCompact α β)

theorem ContinuousMap.uniformEmbedding_equivBoundedOfCompact (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :

UniformEmbedding ⇑(ContinuousMap.equivBoundedOfCompact α β)

def ContinuousMap.addEquivBoundedOfCompact (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] [AddMonoid β] [LipschitzAdd β] :

C(α, β) ≃+ BoundedContinuousFunction α β

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

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem ContinuousMap.addEquivBoundedOfCompact_symm_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] [AddMonoid β] [LipschitzAdd β] :

⇑(AddEquiv.symm (ContinuousMap.addEquivBoundedOfCompact α β)) = ⇑(BoundedContinuousFunction.toContinuousMapAddHom α β)

@[simp]

theorem ContinuousMap.addEquivBoundedOfCompact_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] [AddMonoid β] [LipschitzAdd β] :

⇑(ContinuousMap.addEquivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact

instance ContinuousMap.metricSpace (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :

MetricSpace C(α, β)

Equations

ContinuousMap.metricSpace α β = UniformEmbedding.comapMetricSpace ⇑(ContinuousMap.equivBoundedOfCompact α β) (_ : UniformEmbedding ⇑(ContinuousMap.equivBoundedOfCompact α β))

@[simp]

theorem ContinuousMap.isometryEquivBoundedOfCompact_symm_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :

⇑(IsometryEquiv.symm (ContinuousMap.isometryEquivBoundedOfCompact α β)) = BoundedContinuousFunction.toContinuousMap

@[simp]

theorem ContinuousMap.isometryEquivBoundedOfCompact_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :

⇑(ContinuousMap.isometryEquivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact

@[simp]

theorem ContinuousMap.isometryEquivBoundedOfCompact_toEquiv (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :

(ContinuousMap.isometryEquivBoundedOfCompact α β).toEquiv = ContinuousMap.equivBoundedOfCompact α β

def ContinuousMap.isometryEquivBoundedOfCompact (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] :

C(α, β) ≃ᵢ BoundedContinuousFunction α β

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

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem BoundedContinuousFunction.dist_mkOfCompact {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] (f : C(α, β)) (g : C(α, β)) :

dist (BoundedContinuousFunction.mkOfCompact f) (BoundedContinuousFunction.mkOfCompact g) = dist f g

@[simp]

theorem BoundedContinuousFunction.dist_toContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) :

dist f.toContinuousMap g.toContinuousMap = dist f g

theorem ContinuousMap.dist_apply_le_dist {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} (x : α) :

dist (f x) (g x) ≤ dist f g

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

theorem ContinuousMap.dist_le {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} {C : ℝ} (C0 : 0 ≤ C) :

dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C

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

theorem ContinuousMap.dist_le_iff_of_nonempty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} {C : ℝ} [Nonempty α] :

dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C

theorem ContinuousMap.dist_lt_iff_of_nonempty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} {C : ℝ} [Nonempty α] :

dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C

theorem ContinuousMap.dist_lt_of_nonempty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} {C : ℝ} [Nonempty α] (w : ∀ (x : α), dist (f x) (g x) < C) :

dist f g < C

theorem ContinuousMap.dist_lt_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] {f : C(α, β)} {g : C(α, β)} {C : ℝ} (C0 : 0 < C) :

dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C

instance ContinuousMap.instCompleteSpaceContinuousMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceCompactConvergenceUniformSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompactSpace α] [MetricSpace β] [CompleteSpace β] :

CompleteSpace C(α, β)

Equations

(_ : CompleteSpace C(α, β)) = (_ : CompleteSpace C(α, β))

instance ContinuousMap.instNormContinuousMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroup {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] :

Equations

ContinuousMap.instNormContinuousMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroup = { norm := fun (x : C(α, E)) => dist x 0 }

@[simp]

theorem BoundedContinuousFunction.norm_mkOfCompact {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) :

‖BoundedContinuousFunction.mkOfCompact f‖ = ‖f‖

@[simp]

theorem BoundedContinuousFunction.norm_toContinuousMap_eq {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : BoundedContinuousFunction α E) :

‖f.toContinuousMap‖ = ‖f‖

instance ContinuousMap.instNormedAddCommGroupContinuousMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroup {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] :

NormedAddCommGroup C(α, E)

Equations

One or more equations did not get rendered due to their size.

instance ContinuousMap.instNormOneClassContinuousMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupInstNormContinuousMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupInstOneContinuousMap {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] [Nonempty α] [One E] [NormOneClass E] :

NormOneClass C(α, E)

Equations

(_ : NormOneClass C(α, E)) = (_ : NormOneClass C(α, E))

theorem ContinuousMap.norm_coe_le_norm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) (x : α) :

‖f x‖ ≤ ‖f‖

theorem ContinuousMap.dist_le_two_norm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) (x : α) (y : α) :

dist (f x) (f y) ≤ 2 * ‖f‖

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

theorem ContinuousMap.norm_le {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (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 ContinuousMap.norm_le_of_nonempty {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) [Nonempty α] {M : ℝ} :

‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M

theorem ContinuousMap.norm_lt_iff {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) {M : ℝ} (M0 : 0 < M) :

‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

theorem ContinuousMap.nnnorm_lt_iff {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) {M : NNReal} (M0 : 0 < M) :

‖f‖₊ < M ↔ ∀ (x : α), ‖f x‖₊ < M

theorem ContinuousMap.norm_lt_iff_of_nonempty {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) [Nonempty α] {M : ℝ} :

‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

theorem ContinuousMap.nnnorm_lt_iff_of_nonempty {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) [Nonempty α] {M : NNReal} :

‖f‖₊ < M ↔ ∀ (x : α), ‖f x‖₊ < M

theorem ContinuousMap.apply_le_norm {α : Type u_1} [TopologicalSpace α] [CompactSpace α] (f : C(α, ℝ )) (x : α) :

f x ≤ ‖f‖

theorem ContinuousMap.neg_norm_le_apply {α : Type u_1} [TopologicalSpace α] [CompactSpace α] (f : C(α, ℝ )) (x : α) :

-‖f‖ ≤ f x

theorem ContinuousMap.norm_eq_iSup_norm {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (f : C(α, E)) :

‖f‖ = ⨆ (x : α), ‖f x‖

theorem ContinuousMap.norm_restrict_mono_set {E : Type u_3} [NormedAddCommGroup E] {X : Type u_4} [TopologicalSpace X] (f : C(X, E)) {K : TopologicalSpace.Compacts X} {L : TopologicalSpace.Compacts X} (hKL : K ≤ L) :

‖ContinuousMap.restrict (↑K) f‖ ≤ ‖ContinuousMap.restrict (↑L) f‖

instance ContinuousMap.instNormedRingContinuousMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRing {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {R : Type u_4} [NormedRing R] :

NormedRing C(α, R)

Equations

One or more equations did not get rendered due to their size.

instance ContinuousMap.normedSpace {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] {𝕜 : Type u_4} [NormedField 𝕜] [NormedSpace 𝕜 E] :

NormedSpace 𝕜 C(α, E)

Equations

ContinuousMap.normedSpace = NormedSpace.mk (_ : ∀ (c : 𝕜) (f : C(α, E)), ‖c • BoundedContinuousFunction.mkOfCompact f‖ ≤ ‖c‖ * ‖BoundedContinuousFunction.mkOfCompact f‖)

def ContinuousMap.linearIsometryBoundedOfCompact (α : Type u_1) (E : Type u_3) [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (𝕜 : Type u_4) [NormedField 𝕜] [NormedSpace 𝕜 E] :

C(α, E) ≃ₗᵢ[𝕜] BoundedContinuousFunction α E

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

Equations

One or more equations did not get rendered due to their size.

Instances For

def ContinuousMap.evalCLM {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] (𝕜 : Type u_4) [NormedField 𝕜] [NormedSpace 𝕜 E] (x : α) :

C(α, E) →L[𝕜] E

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

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem ContinuousMap.linearIsometryBoundedOfCompact_symm_apply {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] {𝕜 : Type u_4} [NormedField 𝕜] [NormedSpace 𝕜 E] (f : BoundedContinuousFunction α E) :

(LinearIsometryEquiv.symm (ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜)) f = f.toContinuousMap

@[simp]

theorem ContinuousMap.linearIsometryBoundedOfCompact_apply_apply {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] {𝕜 : Type u_4} [NormedField 𝕜] [NormedSpace 𝕜 E] (f : C(α, E)) (a : α) :

((ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜) f) a = f a

@[simp]

theorem ContinuousMap.linearIsometryBoundedOfCompact_toIsometryEquiv {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] {𝕜 : Type u_4} [NormedField 𝕜] [NormedSpace 𝕜 E] :

LinearIsometryEquiv.toIsometryEquiv (ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜) = ContinuousMap.isometryEquivBoundedOfCompact α E

@[simp]

theorem ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] {𝕜 : Type u_4} [NormedField 𝕜] [NormedSpace 𝕜 E] :

↑(ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toLinearEquiv = ContinuousMap.addEquivBoundedOfCompact α E

@[simp]

theorem ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [NormedAddCommGroup E] {𝕜 : Type u_4} [NormedField 𝕜] [NormedSpace 𝕜 E] :

LinearEquiv.toEquiv (ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toLinearEquiv = ContinuousMap.equivBoundedOfCompact α E

instance ContinuousMap.instNormedAlgebraContinuousMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedRingInstNormedRingContinuousMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRing {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {𝕜 : Type u_4} {γ : Type u_5} [NormedField 𝕜] [NormedRing γ] [NormedAlgebra 𝕜 γ] :

NormedAlgebra 𝕜 C(α, γ)

Equations

One or more equations did not get rendered due to their size.

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

theorem ContinuousMap.uniform_continuity {α : Type u_1} {β : Type u_2} [MetricSpace α] [CompactSpace α] [MetricSpace β] (f : C(α, β)) (ε : ℝ) (h : 0 < ε) :

∃ δ > 0, ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε

def ContinuousMap.modulus {α : Type u_1} {β : Type u_2} [MetricSpace α] [CompactSpace α] [MetricSpace β] (f : C(α, β)) (ε : ℝ) (h : 0 < ε) :

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

Equations

ContinuousMap.modulus f ε h = Classical.choose (_ : ∃ δ > 0, ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε)

Instances For

theorem ContinuousMap.modulus_pos {α : Type u_1} {β : Type u_2} [MetricSpace α] [CompactSpace α] [MetricSpace β] (f : C(α, β)) {ε : ℝ} {h : 0 < ε} :

0 < ContinuousMap.modulus f ε h

theorem ContinuousMap.dist_lt_of_dist_lt_modulus {α : Type u_1} {β : Type u_2} [MetricSpace α] [CompactSpace α] [MetricSpace β] (f : C(α, β)) (ε : ℝ) (h : 0 < ε) {a : α} {b : α} (w : dist a b < ContinuousMap.modulus f ε h) :

dist (f a) (f b) < ε

def ContinuousLinearMap.compLeftContinuousCompact (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace X] [CompactSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup β] [NormedSpace 𝕜 β] [NormedAddCommGroup γ] [NormedSpace 𝕜 γ] (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 ContinuousLinearMap.compLeftContinuousBounded, upgraded version of ContinuousLinearMap.compLeftContinuous, similar to LinearMap.compLeft.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem ContinuousLinearMap.toLinear_compLeftContinuousCompact (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace X] [CompactSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup β] [NormedSpace 𝕜 β] [NormedAddCommGroup γ] [NormedSpace 𝕜 γ] (g : β →L[𝕜] γ) :

↑(ContinuousLinearMap.compLeftContinuousCompact X g) = ContinuousLinearMap.compLeftContinuous 𝕜 X g

@[simp]

theorem ContinuousLinearMap.compLeftContinuousCompact_apply (X : Type u_1) {𝕜 : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace X] [CompactSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup β] [NormedSpace 𝕜 β] [NormedAddCommGroup γ] [NormedSpace 𝕜 γ] (g : β →L[𝕜] γ) (f : C(X, β)) (x : X) :

((ContinuousLinearMap.compLeftContinuousCompact X g) f) x = g (f x)

We now setup variations on compRight* 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:

compRightContinuousMap, the bundled continuous map (for this we need X Y compact).
compRightHomeomorph, when we precompose by a homeomorphism.
compRightAlgHom, when T = R is a topological ring.

def ContinuousMap.compRightContinuousMap {X : Type u_1} {Y : Type u_2} (T : Type u_3) [TopologicalSpace X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [MetricSpace T] (f : C(X, Y)) :

C(C(Y, T), C(X, T))

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

Equations

ContinuousMap.compRightContinuousMap T f = ContinuousMap.mk fun (g : C(Y, T)) => ContinuousMap.comp g f

Instances For

@[simp]

theorem ContinuousMap.compRightContinuousMap_apply {X : Type u_1} {Y : Type u_2} (T : Type u_3) [TopologicalSpace X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [MetricSpace T] (f : C(X, Y)) (g : C(Y, T)) :

(ContinuousMap.compRightContinuousMap T f) g = ContinuousMap.comp g f

def ContinuousMap.compRightHomeomorph {X : Type u_1} {Y : Type u_2} (T : Type u_3) [TopologicalSpace X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [MetricSpace T] (f : X ≃ₜ Y) :

C(Y, T) ≃ₜ C(X, T)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem ContinuousMap.compRightAlgHom_continuous {X : Type u_1} {Y : Type u_2} (R : Type u_3) (A : Type u_4) [TopologicalSpace X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [CommSemiring R] [Semiring A] [MetricSpace A] [TopologicalSemiring A] [Algebra R A] (f : C(X, Y)) :

Continuous ⇑(ContinuousMap.compRightAlgHom R A f)

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 ContinuousMap.summable_of_locally_summable_norm {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {E : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] {ι : Type u_3} {F : ι → C(X, E)} (hF : ∀ (K : TopologicalSpace.Compacts X), Summable fun (i : ι) => ‖ContinuousMap.restrict (↑K) (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 BoundedContinuousFunction.mkOfCompact_star {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [NormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] [CompactSpace α] (f : C(α, β)) :

BoundedContinuousFunction.mkOfCompact (star f) = star (BoundedContinuousFunction.mkOfCompact f)