mathlib3 documentation

topology.continuous_function.bounded

Bounded continuous functions #

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

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

source
structure bounded_continuous_function (α : Type u) (β : Type v) [topological_space α] [pseudo_metric_space β] :
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
source
@[instance]
def bounded_continuous_map_class.to_continuous_map_class (F : Type u_2) (α : Type u_3) (β : Type u_4) [topological_space α] [pseudo_metric_space β] [self : bounded_continuous_map_class F α β] :
continuous_map_class F α β
source
@[class]
structure bounded_continuous_map_class (F : Type u_2) (α : Type u_3) (β : Type u_4) [topological_space α] [pseudo_metric_space β] :
Type (max u_2 u_3 u_4)

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
source
@[protected, instance]
def bounded_continuous_function.bounded_continuous_map_class {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] :
bounded_continuous_map_class (bounded_continuous_function α β) α β
Equations
source
@[protected, instance]
def bounded_continuous_function.has_coe_to_fun {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] :
has_coe_to_fun (bounded_continuous_function α β) (λ (_x : bounded_continuous_function α β), α → β)

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

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

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

Equations
source
@[protected]
theorem bounded_continuous_function.bounded {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (f : bounded_continuous_function α β) :
∃ (C : ℝ), ∀ (x y : α), has_dist.dist (⇑f x) (⇑f y) ≤ C
source
@[protected]
theorem bounded_continuous_function.continuous {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (f : bounded_continuous_function α β) :
continuous ⇑f
source
@[ext]
theorem bounded_continuous_function.ext {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} (h : ∀ (x : α), ⇑f x = ⇑g x) :
f = g
source
theorem bounded_continuous_function.bounded_range {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (f : bounded_continuous_function α β) :
metric.bounded (set.range ⇑f)
source
theorem bounded_continuous_function.bounded_image {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (f : bounded_continuous_function α β) (s : set α) :
metric.bounded (⇑f '' s)
source
theorem bounded_continuous_function.eq_of_empty {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [is_empty α] (f g : bounded_continuous_function α β) :
f = g
source
def bounded_continuous_function.mk_of_bound {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (f : C(α, β)) (C : ℝ) (h : ∀ (x y : α), has_dist.dist (⇑f x) (⇑f y) ≤ C) :
bounded_continuous_function α β

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

Equations
source
@[simp]
theorem bounded_continuous_function.mk_of_bound_coe {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f : C(α, β)} {C : ℝ} {h : ∀ (x y : α), has_dist.dist (⇑f x) (⇑f y) ≤ C} :
⇑(bounded_continuous_function.mk_of_bound f C h) = ⇑f
source
def bounded_continuous_function.mk_of_compact {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [compact_space α] (f : C(α, β)) :
bounded_continuous_function α β

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

Equations
source
@[simp]
theorem bounded_continuous_function.mk_of_compact_apply {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [compact_space α] (f : C(α, β)) (a : α) :
⇑(bounded_continuous_function.mk_of_compact f) a = ⇑f a
source
@[simp]
theorem bounded_continuous_function.mk_of_discrete_apply {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [discrete_topology α] (f : α → β) (C : ℝ) (h : ∀ (x y : α), has_dist.dist (f x) (f y) ≤ C) (ᾰ : α) :
⇑(bounded_continuous_function.mk_of_discrete f C h) ᾰ = f ᾰ
source
@[simp]
theorem bounded_continuous_function.mk_of_discrete_to_continuous_map_apply {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [discrete_topology α] (f : α → β) (C : ℝ) (h : ∀ (x y : α), has_dist.dist (f x) (f y) ≤ C) (ᾰ : α) :
⇑((bounded_continuous_function.mk_of_discrete f C h).to_continuous_map) ᾰ = f ᾰ
source
def bounded_continuous_function.mk_of_discrete {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [discrete_topology α] (f : α → β) (C : ℝ) (h : ∀ (x y : α), has_dist.dist (f x) (f y) ≤ C) :
bounded_continuous_function α β

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
source
@[protected, instance]
noncomputable def bounded_continuous_function.has_dist {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] :
has_dist (bounded_continuous_function α β)

The uniform distance between two bounded continuous functions

Equations
source
theorem bounded_continuous_function.dist_eq {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} :
has_dist.dist f g = has_Inf.Inf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) ≤ C}
source
theorem bounded_continuous_function.dist_set_exists {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} :
∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) ≤ C
source
theorem bounded_continuous_function.dist_coe_le_dist {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} (x : α) :
has_dist.dist (⇑f x) (⇑g x) ≤ has_dist.dist f g

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

source
theorem bounded_continuous_function.dist_le {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} {C : ℝ} (C0 : 0 ≤ C) :
has_dist.dist f g ≤ C ↔ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) ≤ C

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

source
theorem bounded_continuous_function.dist_le_iff_of_nonempty {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} {C : ℝ} [nonempty α] :
has_dist.dist f g ≤ C ↔ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) ≤ C
source
theorem bounded_continuous_function.dist_lt_of_nonempty_compact {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} {C : ℝ} [nonempty α] [compact_space α] (w : ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) < C) :
has_dist.dist f g < C
source
theorem bounded_continuous_function.dist_lt_iff_of_compact {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} {C : ℝ} [compact_space α] (C0 : 0 < C) :
has_dist.dist f g < C ↔ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) < C
source
theorem bounded_continuous_function.dist_lt_iff_of_nonempty_compact {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} {C : ℝ} [nonempty α] [compact_space α] :
has_dist.dist f g < C ↔ ∀ (x : α), has_dist.dist (⇑f x) (⇑g x) < C
source
@[protected, instance]
noncomputable def bounded_continuous_function.pseudo_metric_space {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] :
pseudo_metric_space (bounded_continuous_function α β)

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

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

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

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

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

source
theorem bounded_continuous_function.dist_eq_supr {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} :
has_dist.dist f g = ⨆ (x : α), has_dist.dist (⇑f x) (⇑g x)
source
theorem bounded_continuous_function.nndist_eq_supr {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {f g : bounded_continuous_function α β} :
has_nndist.nndist f g = ⨆ (x : α), has_nndist.nndist (⇑f x) (⇑g x)
source
theorem bounded_continuous_function.tendsto_iff_tendsto_uniformly {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {ι : Type u_1} {F : ι → bounded_continuous_function α β} {f : bounded_continuous_function α β} {l : filter ι} :
filter.tendsto F l (nhds f) ↔ tendsto_uniformly (λ (i : ι), ⇑(F i)) ⇑f l
source
theorem bounded_continuous_function.inducing_coe_fn {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] :
inducing (⇑uniform_fun.of_fun ∘ coe_fn)

The topology on α →ᵇ β is exactly the topology induced by the natural map to α →ᵤ β.

source
theorem bounded_continuous_function.embedding_coe_fn {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] :
embedding (⇑uniform_fun.of_fun ∘ coe_fn)
source
@[simp]
theorem bounded_continuous_function.const_apply (α : Type u) {β : Type v} [topological_space α] [pseudo_metric_space β] (b : β) :
⇑(bounded_continuous_function.const α b) = function.const α b
source
@[simp]
theorem bounded_continuous_function.const_to_continuous_map (α : Type u) {β : Type v} [topological_space α] [pseudo_metric_space β] (b : β) :
(bounded_continuous_function.const α b).to_continuous_map = continuous_map.const α b
source
def bounded_continuous_function.const (α : Type u) {β : Type v} [topological_space α] [pseudo_metric_space β] (b : β) :
bounded_continuous_function α β

Constant as a continuous bounded function.

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

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

Equations
source
theorem bounded_continuous_function.lipschitz_evalx {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (x : α) :
lipschitz_with 1 (λ (f : bounded_continuous_function α β), ⇑f x)
source
theorem bounded_continuous_function.uniform_continuous_coe {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] :
uniform_continuous coe_fn
source
theorem bounded_continuous_function.continuous_coe {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] :
continuous (λ (f : bounded_continuous_function α β) (x : α), ⇑f x)
source
@[continuity]
theorem bounded_continuous_function.continuous_eval_const {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {x : α} :
continuous (λ (f : bounded_continuous_function α β), ⇑f x)

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

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

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

source
@[protected, instance]
def bounded_continuous_function.complete_space {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [complete_space β] :
complete_space (bounded_continuous_function α β)

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

source
def bounded_continuous_function.comp_continuous {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_1} [topological_space δ] (f : bounded_continuous_function α β) (g : C(δ, α)) :
bounded_continuous_function δ β

Composition of a bounded continuous function and a continuous function.

Equations
source
@[simp]
theorem bounded_continuous_function.coe_comp_continuous {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_1} [topological_space δ] (f : bounded_continuous_function α β) (g : C(δ, α)) :
⇑(f.comp_continuous g) = ⇑f ∘ ⇑g
source
@[simp]
theorem bounded_continuous_function.comp_continuous_apply {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_1} [topological_space δ] (f : bounded_continuous_function α β) (g : C(δ, α)) (x : δ) :
⇑(f.comp_continuous g) x = ⇑f (⇑g x)
source
theorem bounded_continuous_function.lipschitz_comp_continuous {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_1} [topological_space δ] (g : C(δ, α)) :
lipschitz_with 1 (λ (f : bounded_continuous_function α β), f.comp_continuous g)
source
theorem bounded_continuous_function.continuous_comp_continuous {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_1} [topological_space δ] (g : C(δ, α)) :
continuous (λ (f : bounded_continuous_function α β), f.comp_continuous g)
source
def bounded_continuous_function.restrict {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (f : bounded_continuous_function α β) (s : set α) :
bounded_continuous_function ↥s β

Restrict a bounded continuous function to a set.

Equations
source
@[simp]
theorem bounded_continuous_function.coe_restrict {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (f : bounded_continuous_function α β) (s : set α) :
⇑(f.restrict s) = ⇑f ∘ coe
source
@[simp]
theorem bounded_continuous_function.restrict_apply {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (f : bounded_continuous_function α β) (s : set α) (x : ↥s) :
⇑(f.restrict s) x = ⇑f ↑x
source
def bounded_continuous_function.comp {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [pseudo_metric_space β] [pseudo_metric_space γ] (G : β → γ) {C : nnreal} (H : lipschitz_with C G) (f : bounded_continuous_function α β) :
bounded_continuous_function α γ

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

Equations
source
theorem bounded_continuous_function.lipschitz_comp {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [pseudo_metric_space β] [pseudo_metric_space γ] {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
lipschitz_with C (bounded_continuous_function.comp G H)

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

source
theorem bounded_continuous_function.uniform_continuous_comp {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [pseudo_metric_space β] [pseudo_metric_space γ] {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
uniform_continuous (bounded_continuous_function.comp G H)

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

source
theorem bounded_continuous_function.continuous_comp {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [pseudo_metric_space β] [pseudo_metric_space γ] {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
continuous (bounded_continuous_function.comp G H)

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

source
def bounded_continuous_function.cod_restrict {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] (s : set β) (f : bounded_continuous_function α β) (H : ∀ (x : α), ⇑f x ∈ s) :
bounded_continuous_function α ↥s

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

Equations
source
noncomputable def bounded_continuous_function.extend {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_2} [topological_space δ] [discrete_topology δ] (f : α ↪ δ) (g : bounded_continuous_function α β) (h : bounded_continuous_function δ β) :
bounded_continuous_function δ β

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
source
@[simp]
theorem bounded_continuous_function.extend_apply {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_2} [topological_space δ] [discrete_topology δ] (f : α ↪ δ) (g : bounded_continuous_function α β) (h : bounded_continuous_function δ β) (x : α) :
⇑(bounded_continuous_function.extend f g h) (⇑f x) = ⇑g x
source
@[simp]
theorem bounded_continuous_function.extend_comp {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_2} [topological_space δ] [discrete_topology δ] (f : α ↪ δ) (g : bounded_continuous_function α β) (h : bounded_continuous_function δ β) :
⇑(bounded_continuous_function.extend f g h) ∘ ⇑f = ⇑g
source
theorem bounded_continuous_function.extend_apply' {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_2} [topological_space δ] [discrete_topology δ] {f : α ↪ δ} {x : δ} (hx : x ∉ set.range ⇑f) (g : bounded_continuous_function α β) (h : bounded_continuous_function δ β) :
⇑(bounded_continuous_function.extend f g h) x = ⇑h x
source
theorem bounded_continuous_function.extend_of_empty {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_2} [topological_space δ] [discrete_topology δ] [is_empty α] (f : α ↪ δ) (g : bounded_continuous_function α β) (h : bounded_continuous_function δ β) :
bounded_continuous_function.extend f g h = h
source
@[simp]
theorem bounded_continuous_function.dist_extend_extend {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_2} [topological_space δ] [discrete_topology δ] (f : α ↪ δ) (g₁ g₂ : bounded_continuous_function α β) (h₁ h₂ : bounded_continuous_function δ β) :
has_dist.dist (bounded_continuous_function.extend f g₁ h₁) (bounded_continuous_function.extend f g₂ h₂) = linear_order.max (has_dist.dist g₁ g₂) (has_dist.dist (h₁.restrict (set.range ⇑f)ᶜ) (h₂.restrict (set.range ⇑f)ᶜ))
source
theorem bounded_continuous_function.isometry_extend {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] {δ : Type u_2} [topological_space δ] [discrete_topology δ] (f : α ↪ δ) (h : bounded_continuous_function δ β) :
isometry (λ (g : bounded_continuous_function α β), bounded_continuous_function.extend f g h)
source
theorem bounded_continuous_function.arzela_ascoli₁ {α : Type u} {β : Type v} [topological_space α] [compact_space α] [pseudo_metric_space β] [compact_space β] (A : set (bounded_continuous_function α β)) (closed : is_closed A) (H : equicontinuous coe_fn) :
is_compact A

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

source
theorem bounded_continuous_function.arzela_ascoli₂ {α : Type u} {β : Type v} [topological_space α] [compact_space α] [pseudo_metric_space β] (s : set β) (hs : is_compact s) (A : set (bounded_continuous_function α β)) (closed : is_closed A) (in_s : ∀ (f : bounded_continuous_function α β) (x : α), f ∈ A → ⇑f x ∈ s) (H : equicontinuous coe_fn) :
is_compact A

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

source
theorem bounded_continuous_function.arzela_ascoli {α : Type u} {β : Type v} [topological_space α] [compact_space α] [pseudo_metric_space β] [t2_space β] (s : set β) (hs : is_compact s) (A : set (bounded_continuous_function α β)) (in_s : ∀ (f : bounded_continuous_function α β) (x : α), f ∈ A → ⇑f x ∈ s) (H : equicontinuous coe_fn) :
is_compact (closure A)

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

source
@[protected, instance]
def bounded_continuous_function.has_zero {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [has_zero β] :
has_zero (bounded_continuous_function α β)
Equations
source
@[protected, instance]
def bounded_continuous_function.has_one {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [has_one β] :
has_one (bounded_continuous_function α β)
Equations
source
@[simp]
theorem bounded_continuous_function.coe_zero {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [has_zero β] :
⇑0 = 0
source
@[simp]
theorem bounded_continuous_function.coe_one {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [has_one β] :
⇑1 = 1
source
@[simp]
theorem bounded_continuous_function.mk_of_compact_one {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [has_one β] [compact_space α] :
bounded_continuous_function.mk_of_compact 1 = 1
source
@[simp]
theorem bounded_continuous_function.mk_of_compact_zero {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [has_zero β] [compact_space α] :
bounded_continuous_function.mk_of_compact 0 = 0
source
theorem bounded_continuous_function.forall_coe_one_iff_one {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [has_one β] (f : bounded_continuous_function α β) :
(∀ (x : α), ⇑f x = 1) ↔ f = 1
source
theorem bounded_continuous_function.forall_coe_zero_iff_zero {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [has_zero β] (f : bounded_continuous_function α β) :
(∀ (x : α), ⇑f x = 0) ↔ f = 0
source
@[simp]
theorem bounded_continuous_function.zero_comp_continuous {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [pseudo_metric_space β] [has_zero β] [topological_space γ] (f : C(γ, α)) :
0.comp_continuous f = 0
source
@[simp]
theorem bounded_continuous_function.one_comp_continuous {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [pseudo_metric_space β] [has_one β] [topological_space γ] (f : C(γ, α)) :
1.comp_continuous f = 1
source
@[protected, instance]
noncomputable def bounded_continuous_function.has_add {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] :
has_add (bounded_continuous_function α β)

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

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

Coercion of a normed_add_group_hom is an add_monoid_hom. Similar to add_monoid_hom.coe_fn.

Equations
source
@[simp]
theorem bounded_continuous_function.to_continuous_map_add_hom_apply (α : Type u) (β : Type v) [topological_space α] [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] (self : bounded_continuous_function α β) :
⇑(bounded_continuous_function.to_continuous_map_add_hom α β) self = self.to_continuous_map
source
def bounded_continuous_function.to_continuous_map_add_hom (α : Type u) (β : Type v) [topological_space α] [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] :
bounded_continuous_function α β →+ C(α, β)

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

Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.add_comm_monoid {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [add_comm_monoid β] [has_lipschitz_add β] :
add_comm_monoid (bounded_continuous_function α β)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.add_add_comm_monoid {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [add_comm_monoid β] [has_lipschitz_add β] :
add_comm_monoid (bounded_continuous_function α β)
Equations
source
@[simp]
theorem bounded_continuous_function.coe_sum {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [add_comm_monoid β] [has_lipschitz_add β] {ι : Type u_1} (s : finset ι) (f : ι → bounded_continuous_function α β) :
⇑(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), ⇑(f i))
source
theorem bounded_continuous_function.sum_apply {α : Type u} {β : Type v} [topological_space α] [pseudo_metric_space β] [add_comm_monoid β] [has_lipschitz_add β] {ι : Type u_1} (s : finset ι) (f : ι → bounded_continuous_function α β) (a : α) :
⇑(s.sum (λ (i : ι), f i)) a = s.sum (λ (i : ι), ⇑(f i) a)
source
@[protected, instance]
noncomputable def bounded_continuous_function.has_norm {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] :
has_norm (bounded_continuous_function α β)
Equations
source
theorem bounded_continuous_function.norm_def {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) :
‖f‖ = has_dist.dist f 0
source
theorem bounded_continuous_function.norm_eq {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) :
‖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.

source
theorem bounded_continuous_function.norm_eq_of_nonempty {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) [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.

source
@[simp]
theorem bounded_continuous_function.norm_eq_zero_of_empty {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) [h : is_empty α] :
‖f‖ = 0
source
theorem bounded_continuous_function.norm_coe_le_norm {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) (x : α) :
‖⇑f x‖ ≤ ‖f‖
source
theorem bounded_continuous_function.dist_le_two_norm' {β : Type v} {γ : Type w} [seminormed_add_comm_group β] {f : γ → β} {C : ℝ} (hC : ∀ (x : γ), ‖f x‖ ≤ C) (x y : γ) :
has_dist.dist (f x) (f y) ≤ 2 * C
source
theorem bounded_continuous_function.dist_le_two_norm {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) (x y : α) :
has_dist.dist (⇑f x) (⇑f y) ≤ 2 * ‖f‖

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

source
theorem bounded_continuous_function.norm_le {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] {f : bounded_continuous_function α β} {C : ℝ} (C0 : 0 ≤ C) :
‖f‖ ≤ C ↔ ∀ (x : α), ‖⇑f x‖ ≤ C

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

source
theorem bounded_continuous_function.norm_le_of_nonempty {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [nonempty α] {f : bounded_continuous_function α β} {M : ℝ} :
‖f‖ ≤ M ↔ ∀ (x : α), ‖⇑f x‖ ≤ M
source
theorem bounded_continuous_function.norm_lt_iff_of_compact {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [compact_space α] {f : bounded_continuous_function α β} {M : ℝ} (M0 : 0 < M) :
‖f‖ < M ↔ ∀ (x : α), ‖⇑f x‖ < M
source
theorem bounded_continuous_function.norm_lt_iff_of_nonempty_compact {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [nonempty α] [compact_space α] {f : bounded_continuous_function α β} {M : ℝ} :
‖f‖ < M ↔ ∀ (x : α), ‖⇑f x‖ < M
source
theorem bounded_continuous_function.norm_const_le {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (b : β) :
‖bounded_continuous_function.const α b‖ ≤ ‖b‖

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

source
@[simp]
theorem bounded_continuous_function.norm_const_eq {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [h : nonempty α] (b : β) :
‖bounded_continuous_function.const α b‖ = ‖b‖
source
def bounded_continuous_function.of_normed_add_comm_group {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : α → β) (Hf : continuous f) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) :
bounded_continuous_function α β

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

Equations
source
@[simp]
theorem bounded_continuous_function.coe_of_normed_add_comm_group {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : α → β) (Hf : continuous f) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) :
⇑(bounded_continuous_function.of_normed_add_comm_group f Hf C H) = f
source
theorem bounded_continuous_function.norm_of_normed_add_comm_group_le {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] {f : α → β} (hfc : continuous f) {C : ℝ} (hC : 0 ≤ C) (hfC : ∀ (x : α), ‖f x‖ ≤ C) :
‖bounded_continuous_function.of_normed_add_comm_group f hfc C hfC‖ ≤ C
source
def bounded_continuous_function.of_normed_add_comm_group_discrete {α : Type u} {β : Type v} [topological_space α] [discrete_topology α] [seminormed_add_comm_group β] (f : α → β) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) :
bounded_continuous_function α β

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

Equations
source
@[simp]
theorem bounded_continuous_function.coe_of_normed_add_comm_group_discrete {α : Type u} {β : Type v} [topological_space α] [discrete_topology α] [seminormed_add_comm_group β] (f : α → β) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) :
⇑(bounded_continuous_function.of_normed_add_comm_group_discrete f C H) = f
source
def bounded_continuous_function.norm_comp {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) :
bounded_continuous_function α ℝ

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
source
@[simp]
theorem bounded_continuous_function.coe_norm_comp {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) :
⇑(f.norm_comp) = has_norm.norm ∘ ⇑f
source
@[simp]
theorem bounded_continuous_function.norm_norm_comp {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) :
‖f.norm_comp‖ = ‖f‖
source
theorem bounded_continuous_function.bdd_above_range_norm_comp {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) :
bdd_above (set.range (has_norm.norm ∘ ⇑f))
source
theorem bounded_continuous_function.norm_eq_supr_norm {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) :
‖f‖ = ⨆ (x : α), ‖⇑f x‖
source
@[protected, instance]
def bounded_continuous_function.norm_one_class {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [nonempty α] [has_one β] [norm_one_class β] :
norm_one_class (bounded_continuous_function α β)

If ‖(1 : β)‖ = 1, then ‖(1 : α →ᵇ β)‖ = 1 if α is nonempty.

source
@[protected, instance]
noncomputable def bounded_continuous_function.has_neg {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] :
has_neg (bounded_continuous_function α β)

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

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

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

Equations
source
@[simp]
theorem bounded_continuous_function.coe_neg {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) :
⇑-f = -⇑f
source
theorem bounded_continuous_function.neg_apply {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) {x : α} :
(⇑-f) x = -⇑f x
source
@[simp]
theorem bounded_continuous_function.coe_sub {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f g : bounded_continuous_function α β) :
⇑(f - g) = ⇑f - ⇑g
source
theorem bounded_continuous_function.sub_apply {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f g : bounded_continuous_function α β) {x : α} :
⇑(f - g) x = ⇑f x - ⇑g x
source
@[simp]
theorem bounded_continuous_function.mk_of_compact_neg {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [compact_space α] (f : C(α, β)) :
bounded_continuous_function.mk_of_compact (-f) = -bounded_continuous_function.mk_of_compact f
source
@[simp]
theorem bounded_continuous_function.mk_of_compact_sub {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [compact_space α] (f g : C(α, β)) :
bounded_continuous_function.mk_of_compact (f - g) = bounded_continuous_function.mk_of_compact f - bounded_continuous_function.mk_of_compact g
source
@[simp]
theorem bounded_continuous_function.coe_zsmul_rec {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) (z : ℤ) :
⇑(zsmul_rec z f) = z • ⇑f
source
@[protected, instance]
def bounded_continuous_function.has_int_scalar {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] :
has_smul ℤ (bounded_continuous_function α β)
Equations
source
@[simp]
theorem bounded_continuous_function.coe_zsmul {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (r : ℤ) (f : bounded_continuous_function α β) :
⇑(r • f) = r • ⇑f
source
@[simp]
theorem bounded_continuous_function.zsmul_apply {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (r : ℤ) (f : bounded_continuous_function α β) (v : α) :
⇑(r • f) v = r • ⇑f v
source
@[protected, instance]
noncomputable def bounded_continuous_function.add_comm_group {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] :
add_comm_group (bounded_continuous_function α β)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.seminormed_add_comm_group {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] :
seminormed_add_comm_group (bounded_continuous_function α β)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.normed_add_comm_group {α : Type u_1} {β : Type u_2} [topological_space α] [normed_add_comm_group β] :
normed_add_comm_group (bounded_continuous_function α β)
Equations
source
theorem bounded_continuous_function.nnnorm_def {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) :
‖f‖₊ = has_nndist.nndist f 0
source
theorem bounded_continuous_function.nnnorm_coe_le_nnnorm {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) (x : α) :
‖⇑f x‖₊ ≤ ‖f‖₊
source
theorem bounded_continuous_function.nndist_le_two_nnnorm {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) (x y : α) :
has_nndist.nndist (⇑f x) (⇑f y) ≤ 2 * ‖f‖₊
source
theorem bounded_continuous_function.nnnorm_le {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) (C : nnreal) :
‖f‖₊ ≤ C ↔ ∀ (x : α), ‖⇑f x‖₊ ≤ C

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

source
theorem bounded_continuous_function.nnnorm_const_le {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (b : β) :
‖bounded_continuous_function.const α b‖₊ ≤ ‖b‖₊
source
@[simp]
theorem bounded_continuous_function.nnnorm_const_eq {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [h : nonempty α] (b : β) :
‖bounded_continuous_function.const α b‖₊ = ‖b‖₊
source
theorem bounded_continuous_function.nnnorm_eq_supr_nnnorm {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f : bounded_continuous_function α β) :
‖f‖₊ = ⨆ (x : α), ‖⇑f x‖₊
source
theorem bounded_continuous_function.abs_diff_coe_le_dist {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] (f g : bounded_continuous_function α β) {x : α} :
‖⇑f x - ⇑g x‖ ≤ has_dist.dist f g
source
theorem bounded_continuous_function.coe_le_coe_add_dist {α : Type u} [topological_space α] {x : α} {f g : bounded_continuous_function α ℝ} :
⇑f x ≤ ⇑g x + has_dist.dist f g
source
theorem bounded_continuous_function.norm_comp_continuous_le {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [seminormed_add_comm_group β] [topological_space γ] (f : bounded_continuous_function α β) (g : C(γ, α)) :
‖f.comp_continuous g‖ ≤ ‖f‖

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.

source
@[protected, instance]
def bounded_continuous_function.has_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [has_zero 𝕜] [has_zero β] [has_smul 𝕜 β] [has_bounded_smul 𝕜 β] :
has_smul 𝕜 (bounded_continuous_function α β)
Equations
source
@[simp]
theorem bounded_continuous_function.coe_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [has_zero 𝕜] [has_zero β] [has_smul 𝕜 β] [has_bounded_smul 𝕜 β] (c : 𝕜) (f : bounded_continuous_function α β) :
⇑(c • f) = λ (x : α), c • ⇑f x
source
theorem bounded_continuous_function.smul_apply {α : Type u} {β : Type v} {𝕜 : Type u_2} [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [has_zero 𝕜] [has_zero β] [has_smul 𝕜 β] [has_bounded_smul 𝕜 β] (c : 𝕜) (f : bounded_continuous_function α β) (x : α) :
⇑(c • f) x = c • ⇑f x
source
@[protected, instance]
def bounded_continuous_function.is_central_scalar {α : Type u} {β : Type v} {𝕜 : Type u_2} [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [has_zero 𝕜] [has_zero β] [has_smul 𝕜 β] [has_bounded_smul 𝕜 β] [has_smul 𝕜ᵐᵒᵖ β] [is_central_scalar 𝕜 β] :
is_central_scalar 𝕜 (bounded_continuous_function α β)
source
@[protected, instance]
def bounded_continuous_function.has_bounded_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [has_zero 𝕜] [has_zero β] [has_smul 𝕜 β] [has_bounded_smul 𝕜 β] :
has_bounded_smul 𝕜 (bounded_continuous_function α β)
source
@[protected, instance]
def bounded_continuous_function.mul_action {α : Type u} {β : Type v} {𝕜 : Type u_2} [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [monoid_with_zero 𝕜] [has_zero β] [mul_action 𝕜 β] [has_bounded_smul 𝕜 β] :
mul_action 𝕜 (bounded_continuous_function α β)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.distrib_mul_action {α : Type u} {β : Type v} {𝕜 : Type u_2} [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [monoid_with_zero 𝕜] [add_monoid β] [distrib_mul_action 𝕜 β] [has_bounded_smul 𝕜 β] [has_lipschitz_add β] :
distrib_mul_action 𝕜 (bounded_continuous_function α β)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.module {α : Type u} {β : Type v} {𝕜 : Type u_2} [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [semiring 𝕜] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] [has_lipschitz_add β] :
module 𝕜 (bounded_continuous_function α β)
Equations
source
def bounded_continuous_function.eval_clm {α : Type u} {β : Type v} (𝕜 : Type u_2) [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [semiring 𝕜] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] [has_lipschitz_add β] (x : α) :
bounded_continuous_function α β →L[𝕜] β

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

Equations
source
@[simp]
theorem bounded_continuous_function.eval_clm_apply {α : Type u} {β : Type v} (𝕜 : Type u_2) [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [semiring 𝕜] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] [has_lipschitz_add β] (x : α) (f : bounded_continuous_function α β) :
⇑(bounded_continuous_function.eval_clm 𝕜 x) f = ⇑f x
source
@[simp]
theorem bounded_continuous_function.to_continuous_map_linear_map_apply (α : Type u) (β : Type v) (𝕜 : Type u_2) [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [semiring 𝕜] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] [has_lipschitz_add β] (self : bounded_continuous_function α β) :
⇑(bounded_continuous_function.to_continuous_map_linear_map α β 𝕜) self = self.to_continuous_map
source
def bounded_continuous_function.to_continuous_map_linear_map (α : Type u) (β : Type v) (𝕜 : Type u_2) [pseudo_metric_space 𝕜] [topological_space α] [pseudo_metric_space β] [semiring 𝕜] [add_comm_monoid β] [module 𝕜 β] [has_bounded_smul 𝕜 β] [has_lipschitz_add β] :
bounded_continuous_function α β →ₗ[𝕜] 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.

source
@[protected, instance]
noncomputable def bounded_continuous_function.normed_space {α : Type u} {β : Type v} {𝕜 : Type u_2} [topological_space α] [seminormed_add_comm_group β] [normed_field 𝕜] [normed_space 𝕜 β] :
normed_space 𝕜 (bounded_continuous_function α β)
Equations
source
@[protected]
noncomputable def continuous_linear_map.comp_left_continuous_bounded (α : Type u) {β : Type v} {γ : Type w} {𝕜 : Type u_2} [topological_space α] [seminormed_add_comm_group β] [nontrivially_normed_field 𝕜] [normed_space 𝕜 β] [seminormed_add_comm_group γ] [normed_space 𝕜 γ] (g : β →L[𝕜] γ) :
bounded_continuous_function α β →L[𝕜] bounded_continuous_function α γ

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
source
@[simp]
theorem continuous_linear_map.comp_left_continuous_bounded_apply (α : Type u) {β : Type v} {γ : Type w} {𝕜 : Type u_2} [topological_space α] [seminormed_add_comm_group β] [nontrivially_normed_field 𝕜] [normed_space 𝕜 β] [seminormed_add_comm_group γ] [normed_space 𝕜 γ] (g : β →L[𝕜] γ) (f : bounded_continuous_function α β) (x : α) :
⇑(⇑(continuous_linear_map.comp_left_continuous_bounded α g) 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.

source
@[protected, instance]
noncomputable def bounded_continuous_function.has_mul {α : Type u} [topological_space α] {R : Type u_2} [non_unital_semi_normed_ring R] :
has_mul (bounded_continuous_function α R)
Equations
source
@[simp]
theorem bounded_continuous_function.coe_mul {α : Type u} [topological_space α] {R : Type u_2} [non_unital_semi_normed_ring R] (f g : bounded_continuous_function α R) :
⇑(f * g) = ⇑f * ⇑g
source
theorem bounded_continuous_function.mul_apply {α : Type u} [topological_space α] {R : Type u_2} [non_unital_semi_normed_ring R] (f g : bounded_continuous_function α R) (x : α) :
⇑(f * g) x = ⇑f x * ⇑g x
source
@[protected, instance]
noncomputable def bounded_continuous_function.non_unital_ring {α : Type u} [topological_space α] {R : Type u_2} [non_unital_semi_normed_ring R] :
non_unital_ring (bounded_continuous_function α R)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.non_unital_semi_normed_ring {α : Type u} [topological_space α] {R : Type u_2} [non_unital_semi_normed_ring R] :
non_unital_semi_normed_ring (bounded_continuous_function α R)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.non_unital_normed_ring {α : Type u} [topological_space α] {R : Type u_2} [non_unital_normed_ring R] :
non_unital_normed_ring (bounded_continuous_function α R)
Equations
source
@[simp]
theorem bounded_continuous_function.coe_npow_rec {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] (f : bounded_continuous_function α R) (n : ℕ) :
⇑(npow_rec n f) = ⇑f ^ n
source
@[protected, instance]
def bounded_continuous_function.has_nat_pow {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] :
has_pow (bounded_continuous_function α R) ℕ
Equations
source
@[simp]
theorem bounded_continuous_function.coe_pow {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] (n : ℕ) (f : bounded_continuous_function α R) :
⇑(f ^ n) = ⇑f ^ n
source
@[simp]
theorem bounded_continuous_function.pow_apply {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] (n : ℕ) (f : bounded_continuous_function α R) (v : α) :
⇑(f ^ n) v = ⇑f v ^ n
source
@[protected, instance]
def bounded_continuous_function.has_nat_cast {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] :
has_nat_cast (bounded_continuous_function α R)
Equations
source
@[simp, norm_cast]
theorem bounded_continuous_function.coe_nat_cast {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] (n : ℕ) :
⇑↑n = ↑n
source
@[protected, instance]
def bounded_continuous_function.has_int_cast {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] :
has_int_cast (bounded_continuous_function α R)
Equations
source
@[simp, norm_cast]
theorem bounded_continuous_function.coe_int_cast {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] (n : ℤ) :
⇑↑n = ↑n
source
@[protected, instance]
noncomputable def bounded_continuous_function.ring {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] :
ring (bounded_continuous_function α R)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.semi_normed_ring {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_ring R] :
semi_normed_ring (bounded_continuous_function α R)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.normed_ring {α : Type u} [topological_space α] {R : Type u_2} [normed_ring R] :
normed_ring (bounded_continuous_function α 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.

source
@[protected, instance]
noncomputable def bounded_continuous_function.comm_ring {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_comm_ring R] :
comm_ring (bounded_continuous_function α R)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.semi_normed_comm_ring {α : Type u} [topological_space α] {R : Type u_2} [semi_normed_comm_ring R] :
semi_normed_comm_ring (bounded_continuous_function α R)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.normed_comm_ring {α : Type u} [topological_space α] {R : Type u_2} [normed_comm_ring R] :
normed_comm_ring (bounded_continuous_function α R)
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.

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

bounded_continuous_function.const as a ring_hom.

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

source
@[protected, instance]
noncomputable def bounded_continuous_function.has_smul' {α : Type u} {β : Type v} {𝕜 : Type u_2} [normed_field 𝕜] [topological_space α] [seminormed_add_comm_group β] [normed_space 𝕜 β] :
has_smul (bounded_continuous_function α 𝕜) (bounded_continuous_function α β)
Equations
source
@[protected, instance]
noncomputable def bounded_continuous_function.module' {α : Type u} {β : Type v} {𝕜 : Type u_2} [normed_field 𝕜] [topological_space α] [seminormed_add_comm_group β] [normed_space 𝕜 β] :
module (bounded_continuous_function α 𝕜) (bounded_continuous_function α β)
Equations
source
theorem bounded_continuous_function.norm_smul_le {α : Type u} {β : Type v} {𝕜 : Type u_2} [normed_field 𝕜] [topological_space α] [seminormed_add_comm_group β] [normed_space 𝕜 β] (f : bounded_continuous_function α 𝕜) (g : bounded_continuous_function α β) :
‖f • g‖ ≤ ‖f‖ * ‖g‖
source
theorem bounded_continuous_function.nnreal.upper_bound {α : Type u_1} [topological_space α] (f : bounded_continuous_function α nnreal) (x : α) :
⇑f x ≤ has_nndist.nndist f 0

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

source
@[protected, instance]
noncomputable def bounded_continuous_function.star_add_monoid {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [star_add_monoid β] [normed_star_group β] :
star_add_monoid (bounded_continuous_function α β)
Equations
source
@[simp]
theorem bounded_continuous_function.coe_star {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [star_add_monoid β] [normed_star_group β] (f : bounded_continuous_function α β) :
⇑(has_star.star f) = has_star.star ⇑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.

source
@[simp]
theorem bounded_continuous_function.star_apply {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [star_add_monoid β] [normed_star_group β] (f : bounded_continuous_function α β) (x : α) :
⇑(has_star.star f) x = has_star.star (⇑f x)
source
@[protected, instance]
def bounded_continuous_function.normed_star_group {α : Type u} {β : Type v} [topological_space α] [seminormed_add_comm_group β] [star_add_monoid β] [normed_star_group β] :
normed_star_group (bounded_continuous_function α β)
source
@[protected, instance]
def bounded_continuous_function.star_module {α : Type u} {β : Type v} {𝕜 : Type u_2} [normed_field 𝕜] [star_ring 𝕜] [topological_space α] [seminormed_add_comm_group β] [star_add_monoid β] [normed_star_group β] [normed_space 𝕜 β] [star_module 𝕜 β] :
star_module 𝕜 (bounded_continuous_function α β)
source
@[protected, instance]
noncomputable def bounded_continuous_function.star_ring {α : Type u} {β : Type v} [topological_space α] [non_unital_normed_ring β] [star_ring β] [normed_star_group β] :
star_ring (bounded_continuous_function α β)
Equations
source
@[protected, instance]
def bounded_continuous_function.cstar_ring {α : Type u} {β : Type v} [topological_space α] [non_unital_normed_ring β] [star_ring β] [cstar_ring β] :
cstar_ring (bounded_continuous_function α β)
source
@[protected, instance]
def bounded_continuous_function.partial_order {α : Type u} {β : Type v} [topological_space α] [normed_lattice_add_comm_group β] :
partial_order (bounded_continuous_function α β)
Equations
source
@[protected, instance]
def bounded_continuous_function.semilattice_inf {α : Type u} {β : Type v} [topological_space α] [normed_lattice_add_comm_group β] :
semilattice_inf (bounded_continuous_function α β)

Continuous normed lattice group valued functions form a meet-semilattice

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

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

Equations
source
@[simp]
theorem bounded_continuous_function.nnreal_part_coe_fun_eq {α : Type u} [topological_space α] (f : bounded_continuous_function α ℝ) :
⇑(f.nnreal_part) = real.to_nnreal ∘ ⇑f
source
def bounded_continuous_function.nnnorm {α : Type u} [topological_space α] (f : bounded_continuous_function α ℝ) :
bounded_continuous_function α nnreal

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

Equations
source
@[simp]
theorem bounded_continuous_function.nnnorm_coe_fun_eq {α : Type u} [topological_space α] (f : bounded_continuous_function α ℝ) :
⇑(f.nnnorm) = has_nnnorm.nnnorm ∘ ⇑f
source
theorem bounded_continuous_function.self_eq_nnreal_part_sub_nnreal_part_neg {α : Type u} [topological_space α] (f : bounded_continuous_function α ℝ) :
⇑f = coe ∘ ⇑(f.nnreal_part) - coe ∘ ⇑((-f).nnreal_part)

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

source
theorem bounded_continuous_function.abs_self_eq_nnreal_part_add_nnreal_part_neg {α : Type u} [topological_space α] (f : bounded_continuous_function α ℝ) :
has_abs.abs ∘ ⇑f = coe ∘ ⇑(f.nnreal_part) + coe ∘ ⇑((-f).nnreal_part)

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