# mathlibdocumentation

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)  :
Type (max u v)

α →ᵇ β is the type of bounded continuous functions α → β from a topological space to a metric space.

When possible, instead of parametrizing results over (f : α →ᵇ β), you should parametrize over (F : Type*) [bounded_continuous_map_class F α β] (f : F).

When you extend this structure, make sure to extend bounded_continuous_map_class.

Instances for bounded_continuous_function
@[class]
structure bounded_continuous_map_class (F : Type u_2) (α : Type u_3) (β : Type u_4)  :
Type (max u_2 u_3 u_4)
• to_continuous_map_class : β
• map_bounded : ∀ (f : F), ∃ (C : ), ∀ (x y : α), has_dist.dist (f x) (f y) C

bounded_continuous_map_class F α β states that F is a type of bounded continuous maps.

You should also extend this typeclass when you extend bounded_continuous_function.

Instances of this typeclass
Instances of other typeclasses for bounded_continuous_map_class
• bounded_continuous_map_class.has_sizeof_inst
@[protected, instance]
def bounded_continuous_function.has_coe_to_fun {α : Type u} {β : Type v}  :
(λ (_x : , α → β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[protected, instance]
def bounded_continuous_function.has_coe_t {F : Type u_1} {α : Type u} {β : Type v} [ β] :
Equations
@[simp]
theorem bounded_continuous_function.coe_to_continuous_fun {α : Type u} {β : Type v} (f : β) :
def bounded_continuous_function.simps.apply {α : Type u} {β : Type v} (h : β) :
α → β

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
@[protected]
theorem bounded_continuous_function.bounded {α : Type u} {β : Type v} (f : β) :
∃ (C : ), ∀ (x y : α), has_dist.dist (f x) (f y) C
@[protected]
theorem bounded_continuous_function.continuous {α : Type u} {β : Type v} (f : β) :
@[ext]
theorem bounded_continuous_function.ext {α : Type u} {β : Type v} {f g : β} (h : ∀ (x : α), f x = g x) :
f = g
theorem bounded_continuous_function.bounded_range {α : Type u} {β : Type v} (f : β) :
theorem bounded_continuous_function.bounded_image {α : Type u} {β : Type v} (f : β) (s : set α) :
theorem bounded_continuous_function.eq_of_empty {α : Type u} {β : Type v} [is_empty α] (f g : β) :
f = g
def bounded_continuous_function.mk_of_bound {α : Type u} {β : Type v} (f : C(α, β)) (C : ) (h : ∀ (x y : α), has_dist.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} {f : C(α, β)} {C : } {h : ∀ (x y : α), has_dist.dist (f x) (f y) C} :
def bounded_continuous_function.mk_of_compact {α : Type u} {β : Type v} (f : C(α, β)) :

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

Equations
@[simp]
theorem bounded_continuous_function.mk_of_compact_apply {α : Type u} {β : Type v} (f : C(α, β)) (a : α) :
@[simp]
theorem bounded_continuous_function.mk_of_discrete_apply {α : Type u} {β : Type v} (f : α → β) (C : ) (h : ∀ (x y : α), has_dist.dist (f x) (f y) C) (ᾰ : α) :
= f ᾰ
@[simp]
theorem bounded_continuous_function.mk_of_discrete_to_continuous_map_apply {α : Type u} {β : Type v} (f : α → β) (C : ) (h : ∀ (x y : α), has_dist.dist (f x) (f y) C) (ᾰ : α) :
= f ᾰ
def bounded_continuous_function.mk_of_discrete {α : Type u} {β : Type v} (f : α → β) (C : ) (h : ∀ (x y : α), has_dist.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
@[protected, instance]
noncomputable def bounded_continuous_function.has_dist {α : Type u} {β : Type v}  :

The uniform distance between two bounded continuous functions

Equations
theorem bounded_continuous_function.dist_eq {α : Type u} {β : Type v} {f g : β} :
= has_Inf.Inf {C : | 0 C ∀ (x : α), has_dist.dist (f x) (g x) C}
theorem bounded_continuous_function.dist_set_exists {α : Type u} {β : Type v} {f g : β} :
∃ (C : ), 0 C ∀ (x : α), has_dist.dist (f x) (g x) C
theorem bounded_continuous_function.dist_coe_le_dist {α : Type u} {β : Type v} {f g : β} (x : α) :

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

theorem bounded_continuous_function.dist_le {α : Type u} {β : Type v} {f g : β} {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 bounded_continuous_function.dist_le_iff_of_nonempty {α : Type u} {β : Type v} {f g : β} {C : } [nonempty α] :
C ∀ (x : α), has_dist.dist (f x) (g x) C
theorem bounded_continuous_function.dist_lt_of_nonempty_compact {α : Type u} {β : Type v} {f g : β} {C : } [nonempty α] (w : ∀ (x : α), has_dist.dist (f x) (g x) < C) :
< C
theorem bounded_continuous_function.dist_lt_iff_of_compact {α : Type u} {β : Type v} {f g : β} {C : } (C0 : 0 < C) :
< C ∀ (x : α), has_dist.dist (f x) (g x) < C
theorem bounded_continuous_function.dist_lt_iff_of_nonempty_compact {α : Type u} {β : Type v} {f g : β} {C : } [nonempty α]  :
< C ∀ (x : α), has_dist.dist (f x) (g x) < C
@[protected, instance]
noncomputable def bounded_continuous_function.pseudo_metric_space {α : Type u} {β : Type v}  :

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

Equations
@[protected, instance]
noncomputable def bounded_continuous_function.metric_space {α : Type u_1} {β : Type u_2} [metric_space β] :

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

Equations
theorem bounded_continuous_function.nndist_eq {α : Type u} {β : Type v} {f g : β} :
= has_Inf.Inf {C : nnreal | ∀ (x : α), has_nndist.nndist (f x) (g x) C}
theorem bounded_continuous_function.nndist_set_exists {α : Type u} {β : Type v} {f g : β} :
∃ (C : nnreal), ∀ (x : α), has_nndist.nndist (f x) (g x) C
theorem bounded_continuous_function.nndist_coe_le_nndist {α : Type u} {β : Type v} {f g : β} (x : α) :
theorem bounded_continuous_function.dist_zero_of_empty {α : Type u} {β : Type v} {f g : β} [is_empty α] :
= 0

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

theorem bounded_continuous_function.dist_eq_supr {α : Type u} {β : Type v} {f g : β} :
= ⨆ (x : α), has_dist.dist (f x) (g x)
theorem bounded_continuous_function.nndist_eq_supr {α : Type u} {β : Type v} {f g : β} :
= ⨆ (x : α), has_nndist.nndist (f x) (g x)
theorem bounded_continuous_function.tendsto_iff_tendsto_uniformly {α : Type u} {β : Type v} {ι : Type u_1} {F : ι → } {f : β} {l : filter ι} :
(nhds f) tendsto_uniformly (λ (i : ι), (F i)) f l
@[simp]
theorem bounded_continuous_function.const_apply (α : Type u) {β : Type v} (b : β) :
@[simp]
theorem bounded_continuous_function.const_to_continuous_map (α : Type u) {β : Type v} (b : β) :
def bounded_continuous_function.const (α : Type u) {β : Type v} (b : β) :

Constant as a continuous bounded function.

Equations
theorem bounded_continuous_function.const_apply' {α : Type u} {β : Type v} (a : α) (b : β) :
= b
@[protected, instance]
def bounded_continuous_function.inhabited {α : Type u} {β : Type v} [inhabited β] :

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

Equations
theorem bounded_continuous_function.lipschitz_evalx {α : Type u} {β : Type v} (x : α) :
(λ (f : , f x)
theorem bounded_continuous_function.uniform_continuous_coe {α : Type u} {β : Type v}  :
theorem bounded_continuous_function.continuous_coe {α : Type u} {β : Type v}  :
continuous (λ (f : (x : α), f x)
@[continuity]
theorem bounded_continuous_function.continuous_eval_const {α : Type u} {β : Type v} {x : α} :
continuous (λ (f : , f x)

When x is fixed, (f : α →ᵇ β) ↦ f x is continuous

@[continuity]
theorem bounded_continuous_function.continuous_eval {α : Type u} {β : Type v}  :
continuous (λ (p : , (p.fst) p.snd)

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

@[protected, instance]
def bounded_continuous_function.complete_space {α : Type u} {β : Type v}  :

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

@[simp]
theorem bounded_continuous_function.comp_continuous_to_continuous_map {α : Type u} {β : Type v} {δ : Type u_1} (f : β) (g : C(δ, α)) :
def bounded_continuous_function.comp_continuous {α : Type u} {β : Type v} {δ : Type u_1} (f : β) (g : C(δ, α)) :

Composition of a bounded continuous function and a continuous function.

Equations
@[simp]
theorem bounded_continuous_function.comp_continuous_apply {α : Type u} {β : Type v} {δ : Type u_1} (f : β) (g : C(δ, α)) :
theorem bounded_continuous_function.lipschitz_comp_continuous {α : Type u} {β : Type v} {δ : Type u_1} (g : C(δ, α)) :
(λ (f : , f.comp_continuous g)
theorem bounded_continuous_function.continuous_comp_continuous {α : Type u} {β : Type v} {δ : Type u_1} (g : C(δ, α)) :
continuous (λ (f : , f.comp_continuous g)
@[simp]
theorem bounded_continuous_function.restrict_apply {α : Type u} {β : Type v} (f : β) (s : set α) :
(f.restrict s) =
def bounded_continuous_function.restrict {α : Type u} {β : Type v} (f : β) (s : set α) :

Restrict a bounded continuous function to a set.

Equations
def bounded_continuous_function.comp {α : Type u} {β : Type v} {γ : Type w} (G : β → γ) {C : nnreal} (H : 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} {G : β → γ} {C : nnreal} (H : 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} {G : β → γ} {C : nnreal} (H : 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} {G : β → γ} {C : nnreal} (H : G) :

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

def bounded_continuous_function.cod_restrict {α : Type u} {β : Type v} (s : set β) (f : β) (H : ∀ (x : α), f x s) :

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

Equations
noncomputable def bounded_continuous_function.extend {α : Type u} {β : Type v} {δ : Type u_2} (f : α δ) (g : β) (h : β) :

A version of function.extend for bounded continuous maps. We assume that the domain has discrete topology, so we only need to verify boundedness.

Equations
@[simp]
theorem bounded_continuous_function.extend_apply {α : Type u} {β : Type v} {δ : Type u_2} (f : α δ) (g : β) (h : β) (x : α) :
(f x) = g x
@[simp]
theorem bounded_continuous_function.extend_comp {α : Type u} {β : Type v} {δ : Type u_2} (f : α δ) (g : β) (h : β) :
= g
theorem bounded_continuous_function.extend_apply' {α : Type u} {β : Type v} {δ : Type u_2} {f : α δ} {x : δ} (hx : x ) (g : β) (h : β) :
x = h x
theorem bounded_continuous_function.extend_of_empty {α : Type u} {β : Type v} {δ : Type u_2} [is_empty α] (f : α δ) (g : β) (h : β) :
@[simp]
theorem bounded_continuous_function.dist_extend_extend {α : Type u} {β : Type v} {δ : Type u_2} (f : α δ) (g₁ g₂ : β) (h₁ h₂ : β) :
theorem bounded_continuous_function.isometry_extend {α : Type u} {β : Type v} {δ : Type u_2} (f : α δ) (h : β) :
isometry (λ (g : ,
theorem bounded_continuous_function.arzela_ascoli₁ {α : Type u} {β : Type v} (A : set ) (closed : is_closed A) (H : ∀ (x : α) (ε : ), ε > 0(∃ (U : set α) (H : U nhds x), ∀ (y : α), y U∀ (z : α), z U∀ (f : , f Ahas_dist.dist (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} (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 nhds x), ∀ (y : α), y U∀ (z : α), z U∀ (f : , f Ahas_dist.dist (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} [t2_space β] (s : set β) (hs : is_compact s) (A : set ) (in_s : ∀ (f : (x : α), f Af x s) (H : ∀ (x : α) (ε : ), ε > 0(∃ (U : set α) (H : U nhds x), ∀ (y : α), y U∀ (z : α), z U∀ (f : , f Ahas_dist.dist (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} {α : Type u} (b : ) (b_lim : (nhds 0) (nhds 0)) (A : set ) (H : ∀ (x y : α) (f : , f Ahas_dist.dist (f x) (f y) b y)) (x : α) (ε : ) (ε0 : 0 < ε) :
∃ (U : set α) (H : U nhds x), ∀ (y : α), y U∀ (z : α), z U∀ (f : , f Ahas_dist.dist (f y) (f z) < ε
@[protected, instance]
def bounded_continuous_function.has_zero {α : Type u} {β : Type v} [has_zero β] :
Equations
@[protected, instance]
def bounded_continuous_function.has_one {α : Type u} {β : Type v} [has_one β] :
Equations
@[simp]
theorem bounded_continuous_function.coe_zero {α : Type u} {β : Type v} [has_zero β] :
0 = 0
@[simp]
theorem bounded_continuous_function.coe_one {α : Type u} {β : Type v} [has_one β] :
1 = 1
@[simp]
theorem bounded_continuous_function.mk_of_compact_one {α : Type u} {β : Type v} [has_one β]  :
@[simp]
theorem bounded_continuous_function.mk_of_compact_zero {α : Type u} {β : Type v} [has_zero β]  :
theorem bounded_continuous_function.forall_coe_one_iff_one {α : Type u} {β : Type v} [has_one β] (f : β) :
(∀ (x : α), f x = 1) f = 1
theorem bounded_continuous_function.forall_coe_zero_iff_zero {α : Type u} {β : Type v} [has_zero β] (f : β) :
(∀ (x : α), f x = 0) f = 0
@[simp]
theorem bounded_continuous_function.zero_comp_continuous {α : Type u} {β : Type v} {γ : Type w} [has_zero β] (f : C(γ, α)) :
= 0
@[simp]
theorem bounded_continuous_function.one_comp_continuous {α : Type u} {β : Type v} {γ : Type w} [has_one β] (f : C(γ, α)) :
= 1
@[protected, instance]
noncomputable def bounded_continuous_function.has_add {α : Type u} {β : Type v} [add_monoid β]  :

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

Equations
@[simp]
theorem bounded_continuous_function.coe_add {α : Type u} {β : Type v} [add_monoid β] (f g : β) :
(f + g) = f + g
theorem bounded_continuous_function.add_apply {α : Type u} {β : Type v} [add_monoid β] (f g : β) {x : α} :
(f + g) x = f x + g x
@[simp]
theorem bounded_continuous_function.mk_of_compact_add {α : Type u} {β : Type v} [add_monoid β] (f g : C(α, β)) :
theorem bounded_continuous_function.add_comp_continuous {α : Type u} {β : Type v} {γ : Type w} [add_monoid β] (f g : β) (h : C(γ, α)) :
(g + f).comp_continuous h = +
@[simp]
theorem bounded_continuous_function.coe_nsmul_rec {α : Type u} {β : Type v} [add_monoid β] (f : β) (n : ) :
f) = n f
@[protected, instance]
def bounded_continuous_function.has_nat_scalar {α : Type u} {β : Type v} [add_monoid β]  :
Equations
@[simp]
theorem bounded_continuous_function.coe_nsmul {α : Type u} {β : Type v} [add_monoid β] (r : ) (f : β) :
(r f) = r f
@[simp]
theorem bounded_continuous_function.nsmul_apply {α : Type u} {β : Type v} [add_monoid β] (r : ) (f : β) (v : α) :
(r f) v = r f v
@[protected, instance]
noncomputable def bounded_continuous_function.add_monoid {α : Type u} {β : Type v} [add_monoid β]  :
Equations
@[protected, instance]
def bounded_continuous_function.has_lipschitz_add {α : Type u} {β : Type v} [add_monoid β]  :
@[simp]
theorem bounded_continuous_function.coe_fn_add_hom_apply {α : Type u} {β : Type v} [add_monoid β] (x : β) (ᾰ : α) :
def bounded_continuous_function.coe_fn_add_hom {α : Type u} {β : Type v} [add_monoid β]  :
→+ α → β

Equations
@[simp]
theorem bounded_continuous_function.to_continuous_map_add_hom_apply (α : Type u) (β : Type v) [add_monoid β] (self : β) :
def bounded_continuous_function.to_continuous_map_add_hom (α : Type u) (β : Type v) [add_monoid β]  :

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

Equations
@[protected, instance]
noncomputable def bounded_continuous_function.add_comm_monoid {α : Type u} {β : Type v}  :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.add_add_comm_monoid {α : Type u} {β : Type v}  :
Equations
@[simp]
theorem bounded_continuous_function.coe_sum {α : Type u} {β : Type v} {ι : Type u_1} (s : finset ι) (f : ι → ) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
theorem bounded_continuous_function.sum_apply {α : Type u} {β : Type v} {ι : Type u_1} (s : finset ι) (f : ι → ) (a : α) :
(s.sum (λ (i : ι), f i)) a = s.sum (λ (i : ι), (f i) a)
@[protected, instance]
noncomputable def bounded_continuous_function.has_norm {α : Type u} {β : Type v}  :
Equations
theorem bounded_continuous_function.norm_def {α : Type u} {β : Type v} (f : β) :
theorem bounded_continuous_function.norm_eq {α : Type u} {β : Type v} (f : β) :
f = has_Inf.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} (f : β) [h : nonempty α] :
f = has_Inf.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} (f : β) [h : is_empty α] :
theorem bounded_continuous_function.norm_coe_le_norm {α : Type u} {β : Type v} (f : β) (x : α) :
theorem bounded_continuous_function.dist_le_two_norm' {β : Type v} {γ : Type w} {f : γ → β} {C : } (hC : ∀ (x : γ), f x C) (x y : γ) :
has_dist.dist (f x) (f y) 2 * C
theorem bounded_continuous_function.dist_le_two_norm {α : Type u} {β : Type v} (f : β) (x y : α) :

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} {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} [nonempty α] {f : β} {M : } :
f M ∀ (x : α), f x M
theorem bounded_continuous_function.norm_lt_iff_of_compact {α : Type u} {β : Type v} {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} [nonempty α] {f : β} {M : } :
f < M ∀ (x : α), f x < M
theorem bounded_continuous_function.norm_const_le {α : Type u} {β : Type v} (b : β) :

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

@[simp]
theorem bounded_continuous_function.norm_const_eq {α : Type u} {β : Type v} [h : nonempty α] (b : β) :
def bounded_continuous_function.of_normed_add_comm_group {α : Type u} {β : Type v} (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_add_comm_group {α : Type u} {β : Type v} (f : α → β) (Hf : continuous f) (C : ) (H : ∀ (x : α), f x C) :
theorem bounded_continuous_function.norm_of_normed_add_comm_group_le {α : Type u} {β : Type v} {f : α → β} (hfc : continuous f) {C : } (hC : 0 C) (hfC : ∀ (x : α), f x C) :
def bounded_continuous_function.of_normed_add_comm_group_discrete {α : Type u} {β : Type v} (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_add_comm_group_discrete {α : Type u} {β : Type v} (f : α → β) (C : ) (H : ∀ (x : α), f x C) :
noncomputable def bounded_continuous_function.norm_comp {α : Type u} {β : Type v} (f : β) :

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

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

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

Equations
@[protected, instance]
noncomputable def bounded_continuous_function.has_sub {α : Type u} {β : Type v}  :

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

Equations
@[simp]
theorem bounded_continuous_function.coe_neg {α : Type u} {β : Type v} (f : β) :
theorem bounded_continuous_function.neg_apply {α : Type u} {β : Type v} (f : β) {x : α} :
(-f) x = -f x
@[simp]
theorem bounded_continuous_function.coe_sub {α : Type u} {β : Type v} (f g : β) :
(f - g) = f - g
theorem bounded_continuous_function.sub_apply {α : Type u} {β : Type v} (f g : β) {x : α} :
(f - g) x = f x - g x
@[simp]
theorem bounded_continuous_function.mk_of_compact_neg {α : Type u} {β : Type v} (f : C(α, β)) :
@[simp]
theorem bounded_continuous_function.mk_of_compact_sub {α : Type u} {β : Type v} (f g : C(α, β)) :
@[simp]
theorem bounded_continuous_function.coe_zsmul_rec {α : Type u} {β : Type v} (f : β) (z : ) :
f) = z f
@[protected, instance]
def bounded_continuous_function.has_int_scalar {α : Type u} {β : Type v}  :
Equations
@[simp]
theorem bounded_continuous_function.coe_zsmul {α : Type u} {β : Type v} (r : ) (f : β) :
(r f) = r f
@[simp]
theorem bounded_continuous_function.zsmul_apply {α : Type u} {β : Type v} (r : ) (f : β) (v : α) :
(r f) v = r f v
@[protected, instance]
noncomputable def bounded_continuous_function.add_comm_group {α : Type u} {β : Type v}  :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.seminormed_add_comm_group {α : Type u} {β : Type v}  :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.normed_add_comm_group {α : Type u_1} {β : Type u_2}  :
Equations
theorem bounded_continuous_function.nnnorm_def {α : Type u} {β : Type v} (f : β) :
theorem bounded_continuous_function.nnnorm_coe_le_nnnorm {α : Type u} {β : Type v} (f : β) (x : α) :
theorem bounded_continuous_function.nndist_le_two_nnnorm {α : Type u} {β : Type v} (f : β) (x y : α) :
theorem bounded_continuous_function.nnnorm_le {α : Type u} {β : Type v} (f : β) (C : nnreal) :
f∥₊ C ∀ (x : α), f x∥₊ C

The nnnorm of a function is controlled by the supremum of the pointwise nnnorms

theorem bounded_continuous_function.nnnorm_const_le {α : Type u} {β : Type v} (b : β) :
@[simp]
theorem bounded_continuous_function.nnnorm_const_eq {α : Type u} {β : Type v} [h : nonempty α] (b : β) :
theorem bounded_continuous_function.nnnorm_eq_supr_nnnorm {α : Type u} {β : Type v} (f : β) :
f∥₊ = ⨆ (x : α), f x∥₊
theorem bounded_continuous_function.abs_diff_coe_le_dist {α : Type u} {β : Type v} (f g : β) {x : α} :
theorem bounded_continuous_function.coe_le_coe_add_dist {α : Type u} {x : α} {f g : } :
f x g x +
theorem bounded_continuous_function.norm_comp_continuous_le {α : Type u} {β : Type v} {γ : Type w} (f : β) (g : C(γ, α)) :

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

@[protected, instance]
def bounded_continuous_function.has_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [has_zero 𝕜] [has_zero β] [ β] [ β] :
Equations
@[simp]
theorem bounded_continuous_function.coe_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [has_zero 𝕜] [has_zero β] [ β] [ β] (c : 𝕜) (f : β) :
(c f) = λ (x : α), c f x
theorem bounded_continuous_function.smul_apply {α : Type u} {β : Type v} {𝕜 : Type u_2} [has_zero 𝕜] [has_zero β] [ β] [ β] (c : 𝕜) (f : β) (x : α) :
(c f) x = c f x
@[protected, instance]
def bounded_continuous_function.is_central_scalar {α : Type u} {β : Type v} {𝕜 : Type u_2} [has_zero 𝕜] [has_zero β] [ β] [ β] [ β] [ β] :
@[protected, instance]
def bounded_continuous_function.has_bounded_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [has_zero 𝕜] [has_zero β] [ β] [ β] :
@[protected, instance]
def bounded_continuous_function.mul_action {α : Type u} {β : Type v} {𝕜 : Type u_2} [has_zero β] [ β] [ β] :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.distrib_mul_action {α : Type u} {β : Type v} {𝕜 : Type u_2} [add_monoid β] [ β] [ β]  :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.module {α : Type u} {β : Type v} {𝕜 : Type u_2} [semiring 𝕜] [ β] [ β]  :
Equations
def bounded_continuous_function.eval_clm {α : Type u} {β : Type v} (𝕜 : Type u_2) [semiring 𝕜] [ β] [ β] (x : α) :

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_2) [semiring 𝕜] [ β] [ β] (x : α) (f : β) :
= f x
@[simp]
theorem bounded_continuous_function.to_continuous_map_linear_map_apply (α : Type u) (β : Type v) (𝕜 : Type u_2) [semiring 𝕜] [ β] [ β] (self : β) :
def bounded_continuous_function.to_continuous_map_linear_map (α : Type u) (β : Type v) (𝕜 : Type u_2) [semiring 𝕜] [ β] [ β]  :

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.

@[protected, instance]
noncomputable def bounded_continuous_function.normed_space {α : Type u} {β : Type v} {𝕜 : Type u_2} [normed_field 𝕜] [ β] :
Equations
@[protected]
noncomputable def continuous_linear_map.comp_left_continuous_bounded (α : Type u) {β : Type v} {γ : Type w} {𝕜 : Type u_2} [ β] [ γ] (g : β →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_2} [ β] [ γ] (g : β →L[𝕜] γ) (f : β) (x : α) :
= g (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.

@[protected, instance]
noncomputable def bounded_continuous_function.has_mul {α : Type u} {R : Type u_2}  :
Equations
@[simp]
theorem bounded_continuous_function.coe_mul {α : Type u} {R : Type u_2} (f g : R) :
(f * g) = f * g
theorem bounded_continuous_function.mul_apply {α : Type u} {R : Type u_2} (f g : R) (x : α) :
(f * g) x = f x * g x
@[protected, instance]
noncomputable def bounded_continuous_function.non_unital_ring {α : Type u} {R : Type u_2}  :
Equations
• bounded_continuous_function.non_unital_ring = bounded_continuous_function.non_unital_ring._proof_3 bounded_continuous_function.non_unital_ring._proof_4 bounded_continuous_function.non_unital_ring._proof_5 bounded_continuous_function.coe_mul bounded_continuous_function.non_unital_ring._proof_6 bounded_continuous_function.non_unital_ring._proof_7 bounded_continuous_function.non_unital_ring._proof_8 bounded_continuous_function.non_unital_ring._proof_9
@[protected, instance]
noncomputable def bounded_continuous_function.non_unital_semi_normed_ring {α : Type u} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.non_unital_normed_ring {α : Type u} {R : Type u_2}  :
Equations
@[simp]
theorem bounded_continuous_function.coe_npow_rec {α : Type u} {R : Type u_2} (f : R) (n : ) :
(npow_rec n f) = f ^ n
@[protected, instance]
def bounded_continuous_function.has_nat_pow {α : Type u} {R : Type u_2}  :
Equations
@[simp]
theorem bounded_continuous_function.coe_pow {α : Type u} {R : Type u_2} (n : ) (f : R) :
(f ^ n) = f ^ n
@[simp]
theorem bounded_continuous_function.pow_apply {α : Type u} {R : Type u_2} (n : ) (f : R) (v : α) :
(f ^ n) v = f v ^ n
@[protected, instance]
def bounded_continuous_function.has_nat_cast {α : Type u} {R : Type u_2}  :
Equations
@[simp, norm_cast]
theorem bounded_continuous_function.coe_nat_cast {α : Type u} {R : Type u_2} (n : ) :
@[protected, instance]
def bounded_continuous_function.has_int_cast {α : Type u} {R : Type u_2}  :
Equations
@[simp, norm_cast]
theorem bounded_continuous_function.coe_int_cast {α : Type u} {R : Type u_2} (n : ) :
@[protected, instance]
noncomputable def bounded_continuous_function.ring {α : Type u} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.semi_normed_ring {α : Type u} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.normed_ring {α : Type u} {R : Type u_2} [normed_ring R] :
Equations

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

@[protected, instance]
noncomputable def bounded_continuous_function.comm_ring {α : Type u} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.semi_normed_comm_ring {α : Type u} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.normed_comm_ring {α : Type u} {R : Type u_2}  :
Equations

### 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_2} [normed_field 𝕜] [normed_ring γ] [ γ] :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.algebra {α : Type u} {γ : Type w} {𝕜 : Type u_2} [normed_field 𝕜] [normed_ring γ] [ γ] :
Equations
@[simp]
theorem bounded_continuous_function.algebra_map_apply {α : Type u} {γ : Type w} {𝕜 : Type u_2} [normed_field 𝕜] [normed_ring γ] [ γ] (k : 𝕜) (a : α) :
( k) a = k 1
@[protected, instance]
noncomputable def bounded_continuous_function.normed_algebra {α : Type u} {γ : Type w} {𝕜 : Type u_2} [normed_field 𝕜] [normed_ring γ] [ γ] :
Equations

### 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 𝕜.

@[protected, instance]
noncomputable def bounded_continuous_function.has_smul' {α : Type u} {β : Type v} {𝕜 : Type u_2} [normed_field 𝕜] [ β] :
Equations
@[protected, instance]
noncomputable def bounded_continuous_function.module' {α : Type u} {β : Type v} {𝕜 : Type u_2} [normed_field 𝕜] [ β] :
Equations
theorem bounded_continuous_function.norm_smul_le {α : Type u} {β : Type v} {𝕜 : Type u_2} [normed_field 𝕜] [ β] (f : 𝕜) (g : β) :
theorem bounded_continuous_function.nnreal.upper_bound {α : Type u_1} (x : α) :
f x

### Star structures #

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

If 𝕜 is normed field and a ⋆-ring over which β is a normed algebra and a star module, then the space of bounded continuous functions from α to β is a star module.

If β is a ⋆-ring in addition to being a normed ⋆-group, then α →ᵇ β inherits a ⋆-ring structure.

In summary, if β is a C⋆-algebra over 𝕜, then so is α →ᵇ β; note that completeness is guaranteed when β is complete (see bounded_continuous_function.complete).

@[protected, instance]
noncomputable def bounded_continuous_function.star_add_monoid {α : Type u} {β : Type v}  :
Equations
@[simp]
theorem bounded_continuous_function.coe_star {α : Type u} {β : Type v} (f : β) :

The right-hand side of this equality can be parsed star ∘ ⇑f because of the instance pi.has_star. Upon inspecting the goal, one sees ⊢ ⇑(star f) = star ⇑f.

@[simp]
theorem bounded_continuous_function.star_apply {α : Type u} {β : Type v} (f : β) (x : α) :
@[protected, instance]
def bounded_continuous_function.normed_star_group {α : Type u} {β : Type v}  :
@[protected, instance]
def bounded_continuous_function.star_module {α : Type u} {β : Type v} {𝕜 : Type u_2} [normed_field 𝕜] [star_ring 𝕜] [ β] [ β] :
@[protected, instance]
noncomputable def bounded_continuous_function.star_ring {α : Type u} {β : Type v} [star_ring β]  :
Equations
@[protected, instance]
def bounded_continuous_function.cstar_ring {α : Type u} {β : Type v} [star_ring β] [cstar_ring β] :
@[protected, instance]
def bounded_continuous_function.partial_order {α : Type u} {β : Type v}  :
Equations
@[protected, instance]
def bounded_continuous_function.semilattice_inf {α : Type u} {β : Type v}  :

Continuous normed lattice group valued functions form a meet-semilattice

Equations
@[protected, instance]
def bounded_continuous_function.semilattice_sup {α : Type u} {β : Type v}  :
Equations
@[protected, instance]
def bounded_continuous_function.lattice {α : Type u} {β : Type v}  :
Equations
@[simp]
theorem bounded_continuous_function.coe_fn_sup {α : Type u} {β : Type v} (f g : β) :
(f g) = f g
@[simp]
theorem bounded_continuous_function.coe_fn_abs {α : Type u} {β : Type v} (f : β) :
@[protected, instance]
noncomputable def bounded_continuous_function.normed_lattice_add_comm_group {α : Type u} {β : Type v}  :
Equations
noncomputable def bounded_continuous_function.nnreal_part {α : Type u} (f : ) :

The nonnegative part of a bounded continuous -valued function as a bounded continuous ℝ≥0-valued function.

Equations
• f.nnreal_part = bounded_continuous_function.nnreal_part._proof_1 f
@[simp]
noncomputable def bounded_continuous_function.nnnorm {α : Type u} (f : ) :

The absolute value of a bounded continuous -valued function as a bounded continuous ℝ≥0-valued function.

Equations
@[simp]
theorem bounded_continuous_function.nnnorm_coe_fun_eq {α : Type u} (f : ) :

Decompose a bounded continuous function to its positive and negative parts.

Express the absolute value of a bounded continuous function in terms of its positive and negative parts.