mathlib documentation

topology.continuous_function.bounded

Bounded continuous functions #

The type of bounded continuous functions taking values in a metric space, with the uniform distance.

structure bounded_continuous_function (α : Type u) (β : Type v) [topological_space α] [metric_space β] :
Type (max u v)

The type of bounded continuous functions from a topological space to a metric space

@[instance]
Equations
theorem bounded_continuous_function.bounded {α : Type u} {β : Type v} [topological_space α] [metric_space β] (f : α →ᵇ β) :
∃ (C : ), ∀ (x y : α), dist (f x) (f y) C
theorem bounded_continuous_function.continuous {α : Type u} {β : Type v} [topological_space α] [metric_space β] (f : α →ᵇ β) :
@[ext]
theorem bounded_continuous_function.ext {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f g : α →ᵇ β} (H : ∀ (x : α), f x = g x) :
f = g
theorem bounded_continuous_function.ext_iff {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f g : α →ᵇ β} :
f = g ∀ (x : α), f x = g x
theorem bounded_continuous_function.bounded_range {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f : α →ᵇ β} :
def bounded_continuous_function.mk_of_bound {α : Type u} {β : Type v} [topological_space α] [metric_space β] (f : C(α, β)) (C : ) (h : ∀ (x y : α), dist (f x) (f y) C) :
α →ᵇ β

A continuous function with an explicit bound is a bounded continuous function.

Equations
@[simp]
theorem bounded_continuous_function.mk_of_bound_coe {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f : C(α, β)} {C : } {h : ∀ (x y : α), dist (f x) (f y) C} :
def bounded_continuous_function.mk_of_compact {α : Type u} {β : Type v} [topological_space α] [metric_space β] [compact_space α] (f : C(α, β)) :
α →ᵇ β

A continuous function on a compact space is automatically a bounded continuous function.

Equations
@[simp]
def bounded_continuous_function.mk_of_discrete {α : Type u} {β : Type v} [topological_space α] [metric_space β] [discrete_topology α] (f : α → β) (C : ) (h : ∀ (x y : α), dist (f x) (f y) C) :
α →ᵇ β

If a function is bounded on a discrete space, it is automatically continuous, and therefore gives rise to an element of the type of bounded continuous functions

Equations
@[simp]
theorem bounded_continuous_function.mk_of_discrete_apply {α : Type u} {β : Type v} [topological_space α] [metric_space β] [discrete_topology α] (f : α → β) (C : ) (h : ∀ (x y : α), dist (f x) (f y) C) (a : α) :
def bounded_continuous_function.forget_boundedness (α : Type u) (β : Type v) [topological_space α] [metric_space β] :
→ᵇ β)C(α, β)

The map forgetting that a bounded continuous function is bounded.

Equations
@[instance]
def bounded_continuous_function.has_dist {α : Type u} {β : Type v} [topological_space α] [metric_space β] :

The uniform distance between two bounded continuous functions

Equations
theorem bounded_continuous_function.dist_eq {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f g : α →ᵇ β} :
dist f g = Inf {C : | 0 C ∀ (x : α), dist (f x) (g x) C}
theorem bounded_continuous_function.dist_set_exists {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f g : α →ᵇ β} :
∃ (C : ), 0 C ∀ (x : α), dist (f x) (g x) C
theorem bounded_continuous_function.dist_coe_le_dist {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f g : α →ᵇ β} (x : α) :
dist (f x) (g x) dist f g

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

theorem bounded_continuous_function.dist_le {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f g : α →ᵇ β} {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 bounded_continuous_function.dist_le_iff_of_nonempty {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f g : α →ᵇ β} {C : } [nonempty α] :
dist f g C ∀ (x : α), dist (f x) (g x) C
theorem bounded_continuous_function.dist_lt_of_nonempty_compact {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f g : α →ᵇ β} {C : } [nonempty α] [compact_space α] (w : ∀ (x : α), dist (f x) (g x) < C) :
dist f g < C
theorem bounded_continuous_function.dist_lt_iff_of_compact {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f g : α →ᵇ β} {C : } [compact_space α] (C0 : 0 < C) :
dist f g < C ∀ (x : α), dist (f x) (g x) < C
theorem bounded_continuous_function.dist_lt_iff_of_nonempty_compact {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f g : α →ᵇ β} {C : } [nonempty α] [compact_space α] :
dist f g < C ∀ (x : α), dist (f x) (g x) < C
theorem bounded_continuous_function.dist_zero_of_empty {α : Type u} {β : Type v} [topological_space α] [metric_space β] {f g : α →ᵇ β} [is_empty α] :
dist f g = 0

On an empty space, bounded continuous functions are at distance 0

@[instance]
def bounded_continuous_function.metric_space {α : Type u} {β : Type v} [topological_space α] [metric_space β] :

The type of bounded continuous functions, with the uniform distance, is a metric space.

Equations
def bounded_continuous_function.const (α : Type u) {β : Type v} [topological_space α] [metric_space β] (b : β) :
α →ᵇ β

Constant as a continuous bounded function.

Equations
@[simp]
theorem bounded_continuous_function.const_apply {α : Type u} {β : Type v} [topological_space α] [metric_space β] (a : α) (b : β) :
@[instance]
def bounded_continuous_function.inhabited {α : Type u} {β : Type v} [topological_space α] [metric_space β] [inhabited β] :

If the target space is inhabited, so is the space of bounded continuous functions

Equations
theorem bounded_continuous_function.continuous_eval {α : Type u} {β : Type v} [topological_space α] [metric_space β] :
continuous (λ (p : →ᵇ β) × α), (p.fst) p.snd)

The evaluation map is continuous, as a joint function of u and x

theorem bounded_continuous_function.continuous_evalx {α : Type u} {β : Type v} [topological_space α] [metric_space β] {x : α} :
continuous (λ (f : α →ᵇ β), f x)

In particular, when x is fixed, f → f x is continuous

@[instance]

Bounded continuous functions taking values in a complete space form a complete space.

def bounded_continuous_function.comp {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [metric_space β] [metric_space γ] (G : β → γ) {C : ℝ≥0} (H : lipschitz_with C G) (f : α →ᵇ β) :
α →ᵇ γ

Composition (in the target) of a bounded continuous function with a Lipschitz map again gives a bounded continuous function

Equations
theorem bounded_continuous_function.lipschitz_comp {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [metric_space β] [metric_space γ] {G : β → γ} {C : ℝ≥0} (H : lipschitz_with C G) :

The composition operator (in the target) with a Lipschitz map is Lipschitz

theorem bounded_continuous_function.uniform_continuous_comp {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [metric_space β] [metric_space γ] {G : β → γ} {C : ℝ≥0} (H : lipschitz_with C G) :

The composition operator (in the target) with a Lipschitz map is uniformly continuous

theorem bounded_continuous_function.continuous_comp {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [metric_space β] [metric_space γ] {G : β → γ} {C : ℝ≥0} (H : lipschitz_with C G) :

The composition operator (in the target) with a Lipschitz map is continuous

def bounded_continuous_function.cod_restrict {α : Type u} {β : Type v} [topological_space α] [metric_space β] (s : set β) (f : α →ᵇ β) (H : ∀ (x : α), f x s) :

Restriction (in the target) of a bounded continuous function taking values in a subset

Equations
theorem bounded_continuous_function.arzela_ascoli₁ {α : Type u} {β : Type v} [topological_space α] [compact_space α] [metric_space β] [compact_space β] (A : set →ᵇ β)) (closed : is_closed A) (H : ∀ (x : α) (ε : ), ε > 0(∃ (U : set α) (H : U 𝓝 x), ∀ (y z : α), y Uz U∀ (f : α →ᵇ β), f Adist (f y) (f z) < ε)) :

First version, with pointwise equicontinuity and range in a compact space

theorem bounded_continuous_function.arzela_ascoli₂ {α : Type u} {β : Type v} [topological_space α] [compact_space α] [metric_space β] (s : set β) (hs : is_compact s) (A : set →ᵇ β)) (closed : is_closed A) (in_s : ∀ (f : α →ᵇ β) (x : α), f Af x s) (H : ∀ (x : α) (ε : ), ε > 0(∃ (U : set α) (H : U 𝓝 x), ∀ (y z : α), y Uz U∀ (f : α →ᵇ β), f Adist (f y) (f z) < ε)) :

Second version, with pointwise equicontinuity and range in a compact subset

theorem bounded_continuous_function.arzela_ascoli {α : Type u} {β : Type v} [topological_space α] [compact_space α] [metric_space β] (s : set β) (hs : is_compact s) (A : set →ᵇ β)) (in_s : ∀ (f : α →ᵇ β) (x : α), f Af x s) (H : ∀ (x : α) (ε : ), ε > 0(∃ (U : set α) (H : U 𝓝 x), ∀ (y z : α), y Uz U∀ (f : α →ᵇ β), f Adist (f y) (f z) < ε)) :

Third (main) version, with pointwise equicontinuity and range in a compact subset, but without closedness. The closure is then compact

theorem bounded_continuous_function.equicontinuous_of_continuity_modulus {β : Type v} [metric_space β] {α : Type u} [metric_space α] (b : ) (b_lim : filter.tendsto b (𝓝 0) (𝓝 0)) (A : set →ᵇ β)) (H : ∀ (x y : α) (f : α →ᵇ β), f Adist (f x) (f y) b (dist x y)) (x : α) (ε : ) (ε0 : 0 < ε) :
∃ (U : set α) (H : U 𝓝 x), ∀ (y z : α), y Uz U∀ (f : α →ᵇ β), f Adist (f y) (f z) < ε
@[simp]
theorem bounded_continuous_function.coe_zero {α : Type u} {β : Type v} [topological_space α] [metric_space β] [add_monoid β] :
0 = 0
theorem bounded_continuous_function.forall_coe_zero_iff_zero {α : Type u} {β : Type v} [topological_space α] [metric_space β] [add_monoid β] (f : α →ᵇ β) :
(∀ (x : α), f x = 0) f = 0
@[instance]
def bounded_continuous_function.has_add {α : Type u} {β : Type v} [topological_space α] [metric_space β] [add_monoid β] [has_lipschitz_add β] :
has_add →ᵇ β)

The pointwise sum of two bounded continuous functions is again bounded continuous.

Equations
@[simp]
theorem bounded_continuous_function.coe_add {α : Type u} {β : Type v} [topological_space α] [metric_space β] [add_monoid β] [has_lipschitz_add β] (f g : α →ᵇ β) :
(f + g) = f + g
theorem bounded_continuous_function.add_apply {α : Type u} {β : Type v} [topological_space α] [metric_space β] [add_monoid β] [has_lipschitz_add β] (f g : α →ᵇ β) {x : α} :
(f + g) x = f x + g x
@[simp]

The additive map forgetting that a bounded continuous function is bounded.

Equations
@[simp]
theorem bounded_continuous_function.coe_sum {α : Type u} {β : Type v} [topological_space α] [metric_space β] [add_comm_monoid β] [has_lipschitz_add β] {ι : Type u_1} (s : finset ι) (f : ι → α →ᵇ β) :
∑ (i : ι) in s, f i = ∑ (i : ι) in s, (f i)
theorem bounded_continuous_function.sum_apply {α : Type u} {β : Type v} [topological_space α] [metric_space β] [add_comm_monoid β] [has_lipschitz_add β] {ι : Type u_1} (s : finset ι) (f : ι → α →ᵇ β) (a : α) :
(∑ (i : ι) in s, f i) a = ∑ (i : ι) in s, (f i) a
@[instance]
def bounded_continuous_function.has_norm {α : Type u} {β : Type v} [topological_space α] [normed_group β] :
Equations
theorem bounded_continuous_function.norm_def {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) :
theorem bounded_continuous_function.norm_eq {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) :
f = Inf {C : | 0 C ∀ (x : α), f x C}

The norm of a bounded continuous function is the supremum of ∥f x∥. We use Inf to ensure that the definition works if α has no elements.

theorem bounded_continuous_function.norm_eq_of_nonempty {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) [h : nonempty α] :
f = Inf {C : | ∀ (x : α), f x C}

When the domain is non-empty, we do not need the 0 ≤ C condition in the formula for ∥f∥ as an Inf.

@[simp]
theorem bounded_continuous_function.norm_eq_zero_of_empty {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) [h : is_empty α] :
theorem bounded_continuous_function.norm_coe_le_norm {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) (x : α) :
theorem bounded_continuous_function.dist_le_two_norm' {β : Type v} {γ : Type w} [normed_group β] {f : γ → β} {C : } (hC : ∀ (x : γ), f x C) (x y : γ) :
dist (f x) (f y) 2 * C
theorem bounded_continuous_function.dist_le_two_norm {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) (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 bounded_continuous_function.norm_le {α : Type u} {β : Type v} [topological_space α] [normed_group β] {f : α →ᵇ β} {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 bounded_continuous_function.norm_le_of_nonempty {α : Type u} {β : Type v} [topological_space α] [normed_group β] [nonempty α] {f : α →ᵇ β} {M : } :
f M ∀ (x : α), f x M
theorem bounded_continuous_function.norm_lt_iff_of_compact {α : Type u} {β : Type v} [topological_space α] [normed_group β] [compact_space α] {f : α →ᵇ β} {M : } (M0 : 0 < M) :
f < M ∀ (x : α), f x < M
theorem bounded_continuous_function.norm_lt_iff_of_nonempty_compact {α : Type u} {β : Type v} [topological_space α] [normed_group β] [nonempty α] [compact_space α] {f : α →ᵇ β} {M : } :
f < M ∀ (x : α), f x < M

Norm of const α b is less than or equal to ∥b∥. If α is nonempty, then it is equal to ∥b∥.

@[simp]
def bounded_continuous_function.of_normed_group {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α → β) (Hf : continuous f) (C : ) (H : ∀ (x : α), f x C) :
α →ᵇ β

Constructing a bounded continuous function from a uniformly bounded continuous function taking values in a normed group.

Equations
@[simp]
theorem bounded_continuous_function.coe_of_normed_group {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α → β) (Hf : continuous f) (C : ) (H : ∀ (x : α), f x C) :
theorem bounded_continuous_function.norm_of_normed_group_le {α : Type u} {β : Type v} [topological_space α] [normed_group β] {f : α → β} (hfc : continuous f) {C : } (hC : 0 C) (hfC : ∀ (x : α), f x C) :
def bounded_continuous_function.of_normed_group_discrete {α : Type u} {β : Type v} [topological_space α] [discrete_topology α] [normed_group β] (f : α → β) (C : ) (H : ∀ (x : α), f x C) :
α →ᵇ β

Constructing a bounded continuous function from a uniformly bounded function on a discrete space, taking values in a normed group

Equations
@[simp]
theorem bounded_continuous_function.coe_of_normed_group_discrete {α : Type u} {β : Type v} [topological_space α] [discrete_topology α] [normed_group β] (f : α → β) (C : ) (H : ∀ (x : α), f x C) :
def bounded_continuous_function.norm_comp {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) :

Taking the pointwise norm of a bounded continuous function with values in a normed_group, yields a bounded continuous function with values in ℝ.

Equations
@[simp]
theorem bounded_continuous_function.coe_norm_comp {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) :
@[simp]
theorem bounded_continuous_function.norm_norm_comp {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) :
theorem bounded_continuous_function.norm_eq_supr_norm {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) :
f = ⨆ (x : α), f x
@[instance]
def bounded_continuous_function.has_neg {α : Type u} {β : Type v} [topological_space α] [normed_group β] :
has_neg →ᵇ β)

The pointwise opposite of a bounded continuous function is again bounded continuous.

Equations
@[instance]
def bounded_continuous_function.has_sub {α : Type u} {β : Type v} [topological_space α] [normed_group β] :
has_sub →ᵇ β)

The pointwise difference of two bounded continuous functions is again bounded continuous.

Equations
@[simp]
theorem bounded_continuous_function.coe_neg {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) :
theorem bounded_continuous_function.neg_apply {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f : α →ᵇ β) {x : α} :
(-f) x = -f x
@[instance]
Equations
@[simp]
theorem bounded_continuous_function.coe_sub {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f g : α →ᵇ β) :
(f - g) = f - g
theorem bounded_continuous_function.sub_apply {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f g : α →ᵇ β) {x : α} :
(f - g) x = f x - g x
theorem bounded_continuous_function.abs_diff_coe_le_dist {α : Type u} {β : Type v} [topological_space α] [normed_group β] (f g : α →ᵇ β) {x : α} :
f x - g x dist f g
theorem bounded_continuous_function.coe_le_coe_add_dist {α : Type u} [topological_space α] {x : α} {f g : α →ᵇ } :
f x g x + dist f g

has_bounded_smul (in particular, topological module) structure #

In this section, if β is a metric space and a 𝕜-module whose addition and scalar multiplication are compatible with the metric structure, then we show that the space of bounded continuous functions from α to β inherits a so-called has_bounded_smul structure (in particular, a has_continuous_mul structure, which is the mathlib formulation of being a topological module), by using pointwise operations and checking that they are compatible with the uniform distance.

@[instance]
def bounded_continuous_function.has_scalar {α : Type u} {β : Type v} {𝕜 : Type u_1} [metric_space 𝕜] [semiring 𝕜] [topological_space α] [metric_space β] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] :
has_scalar 𝕜 →ᵇ β)
Equations
@[simp]
theorem bounded_continuous_function.coe_smul {α : Type u} {β : Type v} {𝕜 : Type u_1} [metric_space 𝕜] [semiring 𝕜] [topological_space α] [metric_space β] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] (c : 𝕜) (f : α →ᵇ β) :
(c f) = λ (x : α), c f x
theorem bounded_continuous_function.smul_apply {α : Type u} {β : Type v} {𝕜 : Type u_1} [metric_space 𝕜] [semiring 𝕜] [topological_space α] [metric_space β] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] (c : 𝕜) (f : α →ᵇ β) (x : α) :
(c f) x = c f x
@[instance]
def bounded_continuous_function.has_bounded_smul {α : Type u} {β : Type v} {𝕜 : Type u_1} [metric_space 𝕜] [semiring 𝕜] [topological_space α] [metric_space β] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] :
def bounded_continuous_function.eval_clm {α : Type u} {β : Type v} (𝕜 : Type u_1) [metric_space 𝕜] [semiring 𝕜] [topological_space α] [metric_space β] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] [has_lipschitz_add β] (x : α) :
→ᵇ β) →L[𝕜] β

The evaluation at a point, as a continuous linear map from α →ᵇ β to β.

Equations
@[simp]
theorem bounded_continuous_function.eval_clm_apply {α : Type u} {β : Type v} (𝕜 : Type u_1) [metric_space 𝕜] [semiring 𝕜] [topological_space α] [metric_space β] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] [has_lipschitz_add β] (x : α) (f : α →ᵇ β) :
def bounded_continuous_function.forget_boundedness_linear_map (α : Type u) (β : Type v) (𝕜 : Type u_1) [metric_space 𝕜] [semiring 𝕜] [topological_space α] [metric_space β] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] [has_lipschitz_add β] :
→ᵇ β) →ₗ[𝕜] C(α, β)

The linear map forgetting that a bounded continuous function is bounded.

Equations

Normed space structure #

In this section, if β is a normed space, then we show that the space of bounded continuous functions from α to β inherits a normed space structure, by using pointwise operations and checking that they are compatible with the uniform distance.

@[instance]
def bounded_continuous_function.normed_space {α : Type u} {β : Type v} {𝕜 : Type u_1} [topological_space α] [normed_group β] [normed_field 𝕜] [normed_space 𝕜 β] :
normed_space 𝕜 →ᵇ β)
Equations
def continuous_linear_map.comp_left_continuous_bounded (α : Type u) {β : Type v} {γ : Type w} {𝕜 : Type u_1} [topological_space α] [normed_group β] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 β] [normed_group γ] [normed_space 𝕜 γ] (g : β →L[𝕜] γ) :
→ᵇ β) →L[𝕜] α →ᵇ γ

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

Equations
@[simp]
theorem continuous_linear_map.comp_left_continuous_bounded_apply (α : Type u) {β : Type v} {γ : Type w} {𝕜 : Type u_1} [topological_space α] [normed_group β] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 β] [normed_group γ] [normed_space 𝕜 γ] (g : β →L[𝕜] γ) (f : α →ᵇ β) (x : α) :

Normed ring structure #

In this section, if R is a normed ring, then we show that the space of bounded continuous functions from α to R inherits a normed ring structure, by using pointwise operations and checking that they are compatible with the uniform distance.

@[simp]
theorem bounded_continuous_function.coe_mul {α : Type u} [topological_space α] {R : Type u_1} [normed_ring R] (f g : α →ᵇ R) :
f * g = (f) * g
theorem bounded_continuous_function.mul_apply {α : Type u} [topological_space α] {R : Type u_1} [normed_ring R] (f g : α →ᵇ R) (x : α) :
(f * g) x = (f x) * g x

Normed commutative ring structure #

In this section, if R is a normed commutative ring, then we show that the space of bounded continuous functions from α to R inherits a normed commutative ring structure, by using pointwise operations and checking that they are compatible with the uniform distance.

Normed algebra structure #

In this section, if γ is a normed algebra, then we show that the space of bounded continuous functions from α to γ inherits a normed algebra structure, by using pointwise operations and checking that they are compatible with the uniform distance.

def bounded_continuous_function.C {α : Type u} {γ : Type w} {𝕜 : Type u_1} [normed_field 𝕜] [topological_space α] [normed_ring γ] [normed_algebra 𝕜 γ] :
𝕜 →+* α →ᵇ γ

bounded_continuous_function.const as a ring_hom.

Equations
@[simp]
theorem bounded_continuous_function.algebra_map_apply {α : Type u} {γ : Type w} {𝕜 : Type u_1} [normed_field 𝕜] [topological_space α] [normed_ring γ] [normed_algebra 𝕜 γ] (k : 𝕜) (a : α) :
((algebra_map 𝕜 →ᵇ γ)) k) a = k 1

Structure as normed module over scalar functions #

If β is a normed 𝕜-space, then we show that the space of bounded continuous functions from α to β is naturally a module over the algebra of bounded continuous functions from α to 𝕜.

@[instance]
def bounded_continuous_function.has_scalar' {α : Type u} {β : Type v} {𝕜 : Type u_1} [normed_field 𝕜] [topological_space α] [normed_group β] [normed_space 𝕜 β] :
has_scalar →ᵇ 𝕜) →ᵇ β)
Equations
theorem bounded_continuous_function.norm_smul_le {α : Type u} {β : Type v} {𝕜 : Type u_1} [normed_field 𝕜] [topological_space α] [normed_group β] [normed_space 𝕜 β] (f : α →ᵇ 𝕜) (g : α →ᵇ β) :