Bounded continuous functions

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

structure BoundedContinuousFunction (α : Type u) (β : Type v) [TopologicalSpace α] [PseudoMetricSpace β] extends ContinuousMap : 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*) [BoundedContinuousMapClass F α β] (f : F).

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

• toFun : α → β
• continuous_toFun : Continuous self.toFun
• map_bounded' : ∃ (C : ℝ), ∀ (x y : α), dist (self.toFun x) (self.toFun y) ≤ C

theorem BoundedContinuousFunction.map_bounded' {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (self : BoundedContinuousFunction α β) : ∃ (C : ℝ), ∀ (x y : α), dist (self.toFun x) (self.toFun y) ≤ C

def BoundedContinuousFunction.«term_→ᵇ_» : Lean.TrailingParserDescr

Equations

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

class BoundedContinuousMapClass (F : Type u_2) (α : outParam (Type u_3)) (β : outParam (Type u_4)) [TopologicalSpace α] [PseudoMetricSpace β] [FunLike F α β] extends ContinuousMapClass : Prop

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

You should also extend this typeclass when you extend BoundedContinuousFunction.

• map_continuous : ∀ (f : F), Continuous ⇑f
• map_bounded : ∀ (f : F), ∃ (C : ℝ), ∀ (x y : α), dist (f x) (f y) ≤ C

theorem BoundedContinuousMapClass.map_bounded {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} : ∀ {inst : TopologicalSpace α} {inst_1 : PseudoMetricSpace β} {inst_2 : FunLike F α β} [self : BoundedContinuousMapClass F α β] (f : F), ∃ (C : ℝ), ∀ (x y : α), dist (f x) (f y) ≤ C

instance BoundedContinuousFunction.instFunLike {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : FunLike (BoundedContinuousFunction α β) α β

Equations

• BoundedContinuousFunction.instFunLike = { coe := fun (f : BoundedContinuousFunction α β) => f.toFun, coe_injective' := ⋯ }

instance BoundedContinuousFunction.instBoundedContinuousMapClass {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : BoundedContinuousMapClass (BoundedContinuousFunction α β) α β

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instCoeTC {F : Type u_1} {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [FunLike F α β] [BoundedContinuousMapClass F α β] : CoeTC F (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instCoeTC = { coe := fun (f : F) => { toFun := ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ } }

@[simp]

theorem BoundedContinuousFunction.coe_to_continuous_fun {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) : ⇑f.toContinuousMap = ⇑f

def BoundedContinuousFunction.Simps.apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (h : BoundedContinuousFunction α β) : α → β

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

Equations

• BoundedContinuousFunction.Simps.apply h = ⇑h

theorem BoundedContinuousFunction.bounded {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) : ∃ (C : ℝ), ∀ (x y : α), dist (f x) (f y) ≤ C

theorem BoundedContinuousFunction.continuous {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) : Continuous ⇑f

theorem BoundedContinuousFunction.ext_iff {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} : f = g ↔ ∀ (x : α), f x = g x

theorem BoundedContinuousFunction.ext {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} (h : ∀ (x : α), f x = g x) : f = g

theorem BoundedContinuousFunction.isBounded_range {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) : Bornology.IsBounded (Set.range ⇑f)

theorem BoundedContinuousFunction.isBounded_image {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) (s : Set α) : Bornology.IsBounded (⇑f '' s)

theorem BoundedContinuousFunction.eq_of_empty {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [h : IsEmpty α] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) : f = g

def BoundedContinuousFunction.mkOfBound {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : C(α, β)) (C : ℝ) (h : ∀ (x y : α), dist (f x) (f y) ≤ C) : BoundedContinuousFunction α β

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

Equations

• BoundedContinuousFunction.mkOfBound f C h = { toContinuousMap := f, map_bounded' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.mkOfBound_coe {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : C(α, β)} {C : ℝ} {h : ∀ (x y : α), dist (f x) (f y) ≤ C} : ⇑(BoundedContinuousFunction.mkOfBound f C h) = ⇑f

def BoundedContinuousFunction.mkOfCompact {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [CompactSpace α] (f : C(α, β)) : BoundedContinuousFunction α β

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

Equations

• BoundedContinuousFunction.mkOfCompact f = { toContinuousMap := f, map_bounded' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.mkOfCompact_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [CompactSpace α] (f : C(α, β)) (a : α) : (BoundedContinuousFunction.mkOfCompact f) a = f a

@[simp]

theorem BoundedContinuousFunction.mkOfDiscrete_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [DiscreteTopology α] (f : α → β) (C : ℝ) (h : ∀ (x y : α), dist (f x) (f y) ≤ C) : ∀ (a : α), (BoundedContinuousFunction.mkOfDiscrete f C h) a = f a

@[simp]

theorem BoundedContinuousFunction.mkOfDiscrete_toFun {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [DiscreteTopology α] (f : α → β) (C : ℝ) (h : ∀ (x y : α), dist (f x) (f y) ≤ C) : ∀ (a : α), (BoundedContinuousFunction.mkOfDiscrete f C h) a = f a

def BoundedContinuousFunction.mkOfDiscrete {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [DiscreteTopology α] (f : α → β) (C : ℝ) (h : ∀ (x y : α), dist (f x) (f y) ≤ C) : BoundedContinuousFunction α β

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

• BoundedContinuousFunction.mkOfDiscrete f C h = { toFun := f, continuous_toFun := ⋯, map_bounded' := ⋯ }

instance BoundedContinuousFunction.instDist {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : Dist (BoundedContinuousFunction α β)

The uniform distance between two bounded continuous functions.

Equations

• BoundedContinuousFunction.instDist = { dist := fun (f g : BoundedContinuousFunction α β) => sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} }

theorem BoundedContinuousFunction.dist_eq {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} : dist f g = sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C}

theorem BoundedContinuousFunction.dist_set_exists {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C

theorem BoundedContinuousFunction.dist_coe_le_dist {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} (x : α) : dist (f x) (g x) ≤ dist f g

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

theorem BoundedContinuousFunction.dist_le {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} {C : ℝ} (C0 : 0 ≤ C) : dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C

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

theorem BoundedContinuousFunction.dist_le_iff_of_nonempty {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} {C : ℝ} [Nonempty α] : dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C

theorem BoundedContinuousFunction.dist_lt_of_nonempty_compact {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} {C : ℝ} [Nonempty α] [CompactSpace α] (w : ∀ (x : α), dist (f x) (g x) < C) : dist f g < C

theorem BoundedContinuousFunction.dist_lt_iff_of_compact {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} {C : ℝ} [CompactSpace α] (C0 : 0 < C) : dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C

theorem BoundedContinuousFunction.dist_lt_iff_of_nonempty_compact {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} {C : ℝ} [Nonempty α] [CompactSpace α] : dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C

instance BoundedContinuousFunction.instPseudoMetricSpace {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : PseudoMetricSpace (BoundedContinuousFunction α β)

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

Equations

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

instance BoundedContinuousFunction.instMetricSpace {α : Type u} [TopologicalSpace α] {β : Type u_2} [MetricSpace β] : MetricSpace (BoundedContinuousFunction α β)

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

Equations

• BoundedContinuousFunction.instMetricSpace = MetricSpace.mk ⋯

theorem BoundedContinuousFunction.nndist_eq {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} : nndist f g = sInf {C : NNReal | ∀ (x : α), nndist (f x) (g x) ≤ C}

theorem BoundedContinuousFunction.nndist_set_exists {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} : ∃ (C : NNReal), ∀ (x : α), nndist (f x) (g x) ≤ C

theorem BoundedContinuousFunction.nndist_coe_le_nndist {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} (x : α) : nndist (f x) (g x) ≤ nndist f g

theorem BoundedContinuousFunction.dist_zero_of_empty {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} [IsEmpty α] : dist f g = 0

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

theorem BoundedContinuousFunction.dist_eq_iSup {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} : dist f g = ⨆ (x : α), dist (f x) (g x)

theorem BoundedContinuousFunction.nndist_eq_iSup {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} : nndist f g = ⨆ (x : α), nndist (f x) (g x)

theorem BoundedContinuousFunction.tendsto_iff_tendstoUniformly {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {ι : Type u_2} {F : ι → BoundedContinuousFunction α β} {f : BoundedContinuousFunction α β} {l : Filter ι} : Filter.Tendsto F l (nhds f) ↔ TendstoUniformly (fun (i : ι) => ⇑(F i)) (⇑f) l

theorem BoundedContinuousFunction.isInducing_coeFn {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : IsInducing (⇑UniformFun.ofFun ∘ DFunLike.coe)

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

@[deprecated BoundedContinuousFunction.isInducing_coeFn]

theorem BoundedContinuousFunction.inducing_coeFn {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : IsInducing (⇑UniformFun.ofFun ∘ DFunLike.coe)

Alias of BoundedContinuousFunction.isInducing_coeFn.

---

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

theorem BoundedContinuousFunction.isEmbedding_coeFn {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : IsEmbedding (⇑UniformFun.ofFun ∘ DFunLike.coe)

@[deprecated BoundedContinuousFunction.isEmbedding_coeFn]

theorem BoundedContinuousFunction.embedding_coeFn {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : IsEmbedding (⇑UniformFun.ofFun ∘ DFunLike.coe)

Alias of BoundedContinuousFunction.isEmbedding_coeFn.

@[simp]

theorem BoundedContinuousFunction.const_apply (α : Type u) {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (b : β) : ⇑(BoundedContinuousFunction.const α b) = fun (x : α) => b

@[simp]

theorem BoundedContinuousFunction.const_toFun (α : Type u) {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (b : β) : ⇑(BoundedContinuousFunction.const α b) = fun (x : α) => b

def BoundedContinuousFunction.const (α : Type u) {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (b : β) : BoundedContinuousFunction α β

Constant as a continuous bounded function.

Equations

• BoundedContinuousFunction.const α b = { toContinuousMap := ContinuousMap.const α b, map_bounded' := ⋯ }

theorem BoundedContinuousFunction.const_apply' {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (a : α) (b : β) : (BoundedContinuousFunction.const α b) a = b

instance BoundedContinuousFunction.instInhabited {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Inhabited β] : Inhabited (BoundedContinuousFunction α β)

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

Equations

• BoundedContinuousFunction.instInhabited = { default := BoundedContinuousFunction.const α default }

theorem BoundedContinuousFunction.lipschitz_evalx {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (x : α) : LipschitzWith 1 fun (f : BoundedContinuousFunction α β) => f x

theorem BoundedContinuousFunction.uniformContinuous_coe {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : UniformContinuous DFunLike.coe

theorem BoundedContinuousFunction.continuous_coe {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : Continuous fun (f : BoundedContinuousFunction α β) (x : α) => f x

theorem BoundedContinuousFunction.continuous_eval_const {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {x : α} : Continuous fun (f : BoundedContinuousFunction α β) => f x

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

theorem BoundedContinuousFunction.continuous_eval {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : Continuous fun (p : BoundedContinuousFunction α β × α) => p.1 p.2

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

instance BoundedContinuousFunction.instCompleteSpace {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [CompleteSpace β] : CompleteSpace (BoundedContinuousFunction α β)

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

Equations

• ⋯ = ⋯

def BoundedContinuousFunction.compContinuous {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] (f : BoundedContinuousFunction α β) (g : C(δ, α)) : BoundedContinuousFunction δ β

Composition of a bounded continuous function and a continuous function.

Equations

• f.compContinuous g = { toContinuousMap := f.comp g, map_bounded' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.coe_compContinuous {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] (f : BoundedContinuousFunction α β) (g : C(δ, α)) : ⇑(f.compContinuous g) = ⇑f ∘ ⇑g

@[simp]

theorem BoundedContinuousFunction.compContinuous_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] (f : BoundedContinuousFunction α β) (g : C(δ, α)) (x : δ) : (f.compContinuous g) x = f (g x)

theorem BoundedContinuousFunction.lipschitz_compContinuous {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] (g : C(δ, α)) : LipschitzWith 1 fun (f : BoundedContinuousFunction α β) => f.compContinuous g

theorem BoundedContinuousFunction.continuous_compContinuous {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] (g : C(δ, α)) : Continuous fun (f : BoundedContinuousFunction α β) => f.compContinuous g

def BoundedContinuousFunction.restrict {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) (s : Set α) : BoundedContinuousFunction (↑s) β

Restrict a bounded continuous function to a set.

Equations

• f.restrict s = f.compContinuous (ContinuousMap.restrict s (ContinuousMap.id α))

@[simp]

theorem BoundedContinuousFunction.coe_restrict {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) (s : Set α) : ⇑(f.restrict s) = ⇑f ∘ Subtype.val

@[simp]

theorem BoundedContinuousFunction.restrict_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) (s : Set α) (x : ↑s) : (f.restrict s) x = f ↑x

def BoundedContinuousFunction.comp {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] (G : β → γ) {C : NNReal} (H : LipschitzWith C G) (f : BoundedContinuousFunction α β) : BoundedContinuousFunction α γ

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

Equations

• BoundedContinuousFunction.comp G H f = { toFun := fun (x : α) => G (f x), continuous_toFun := ⋯, map_bounded' := ⋯ }

theorem BoundedContinuousFunction.lipschitz_comp {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] {G : β → γ} {C : NNReal} (H : LipschitzWith C G) : LipschitzWith C (BoundedContinuousFunction.comp G H)

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

theorem BoundedContinuousFunction.uniformContinuous_comp {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] {G : β → γ} {C : NNReal} (H : LipschitzWith C G) : UniformContinuous (BoundedContinuousFunction.comp G H)

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

theorem BoundedContinuousFunction.continuous_comp {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] {G : β → γ} {C : NNReal} (H : LipschitzWith C G) : Continuous (BoundedContinuousFunction.comp G H)

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

def BoundedContinuousFunction.codRestrict {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (s : Set β) (f : BoundedContinuousFunction α β) (H : ∀ (x : α), f x ∈ s) : BoundedContinuousFunction α ↑s

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

Equations

• BoundedContinuousFunction.codRestrict s f H = { toFun := Set.codRestrict (⇑f) s H, continuous_toFun := ⋯, map_bounded' := ⋯ }

def BoundedContinuousFunction.extend {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] [DiscreteTopology δ] (f : α ↪ δ) (g : BoundedContinuousFunction α β) (h : BoundedContinuousFunction δ β) : BoundedContinuousFunction δ β

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

• BoundedContinuousFunction.extend f g h = { toFun := Function.extend ⇑f ⇑g ⇑h, continuous_toFun := ⋯, map_bounded' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.extend_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] [DiscreteTopology δ] (f : α ↪ δ) (g : BoundedContinuousFunction α β) (h : BoundedContinuousFunction δ β) (x : α) : (BoundedContinuousFunction.extend f g h) (f x) = g x

@[simp]

theorem BoundedContinuousFunction.extend_comp {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] [DiscreteTopology δ] (f : α ↪ δ) (g : BoundedContinuousFunction α β) (h : BoundedContinuousFunction δ β) : ⇑(BoundedContinuousFunction.extend f g h) ∘ ⇑f = ⇑g

theorem BoundedContinuousFunction.extend_apply' {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] [DiscreteTopology δ] {f : α ↪ δ} {x : δ} (hx : x ∉ Set.range ⇑f) (g : BoundedContinuousFunction α β) (h : BoundedContinuousFunction δ β) : (BoundedContinuousFunction.extend f g h) x = h x

theorem BoundedContinuousFunction.extend_of_empty {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] [DiscreteTopology δ] [IsEmpty α] (f : α ↪ δ) (g : BoundedContinuousFunction α β) (h : BoundedContinuousFunction δ β) : BoundedContinuousFunction.extend f g h = h

@[simp]

theorem BoundedContinuousFunction.dist_extend_extend {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] [DiscreteTopology δ] (f : α ↪ δ) (g₁ : BoundedContinuousFunction α β) (g₂ : BoundedContinuousFunction α β) (h₁ : BoundedContinuousFunction δ β) (h₂ : BoundedContinuousFunction δ β) : dist (BoundedContinuousFunction.extend f g₁ h₁) (BoundedContinuousFunction.extend f g₂ h₂) = max (dist g₁ g₂) (dist (h₁.restrict (Set.range ⇑f)ᶜ) (h₂.restrict (Set.range ⇑f)ᶜ))

theorem BoundedContinuousFunction.isometry_extend {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] [DiscreteTopology δ] (f : α ↪ δ) (h : BoundedContinuousFunction δ β) : Isometry fun (g : BoundedContinuousFunction α β) => BoundedContinuousFunction.extend f g h

@[simp]

theorem BoundedContinuousFunction.indicator_toFun {α : Type u} [TopologicalSpace α] (s : Set α) (hs : IsClopen s) (x : α) : (BoundedContinuousFunction.indicator s hs) x = s.indicator 1 x

@[simp]

theorem BoundedContinuousFunction.indicator_apply {α : Type u} [TopologicalSpace α] (s : Set α) (hs : IsClopen s) (x : α) : (BoundedContinuousFunction.indicator s hs) x = s.indicator 1 x

noncomputable def BoundedContinuousFunction.indicator {α : Type u} [TopologicalSpace α] (s : Set α) (hs : IsClopen s) : BoundedContinuousFunction α ℝ

The indicator function of a clopen set, as a bounded continuous function.

Equations

• BoundedContinuousFunction.indicator s hs = { toFun := s.indicator 1, continuous_toFun := ⋯, map_bounded' := ⋯ }

theorem BoundedContinuousFunction.arzela_ascoli₁ {α : Type u} {β : Type v} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] [CompactSpace β] (A : Set (BoundedContinuousFunction α β)) (closed : IsClosed A) (H : Equicontinuous fun (x : ↑A) => ⇑↑x) : IsCompact A

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

theorem BoundedContinuousFunction.arzela_ascoli₂ {α : Type u} {β : Type v} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] (s : Set β) (hs : IsCompact s) (A : Set (BoundedContinuousFunction α β)) (closed : IsClosed A) (in_s : ∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous fun (x : ↑A) => ⇑↑x) : IsCompact A

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

theorem BoundedContinuousFunction.arzela_ascoli {α : Type u} {β : Type v} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] [T2Space β] (s : Set β) (hs : IsCompact s) (A : Set (BoundedContinuousFunction α β)) (in_s : ∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous fun (x : ↑A) => ⇑↑x) : IsCompact (closure A)

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

instance BoundedContinuousFunction.instZero {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] : Zero (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instZero = { zero := BoundedContinuousFunction.const α 0 }

instance BoundedContinuousFunction.instOne {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [One β] : One (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instOne = { one := BoundedContinuousFunction.const α 1 }

@[simp]

theorem BoundedContinuousFunction.coe_zero {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] : ⇑0 = 0

@[simp]

theorem BoundedContinuousFunction.coe_one {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [One β] : ⇑1 = 1

@[simp]

theorem BoundedContinuousFunction.mkOfCompact_zero {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] [CompactSpace α] : BoundedContinuousFunction.mkOfCompact 0 = 0

@[simp]

theorem BoundedContinuousFunction.mkOfCompact_one {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [One β] [CompactSpace α] : BoundedContinuousFunction.mkOfCompact 1 = 1

theorem BoundedContinuousFunction.forall_coe_zero_iff_zero {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] (f : BoundedContinuousFunction α β) : (∀ (x : α), f x = 0) ↔ f = 0

theorem BoundedContinuousFunction.forall_coe_one_iff_one {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [One β] (f : BoundedContinuousFunction α β) : (∀ (x : α), f x = 1) ↔ f = 1

@[simp]

theorem BoundedContinuousFunction.zero_compContinuous {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] [TopologicalSpace γ] (f : C(γ, α)) : BoundedContinuousFunction.compContinuous 0 f = 0

@[simp]

theorem BoundedContinuousFunction.one_compContinuous {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoMetricSpace β] [One β] [TopologicalSpace γ] (f : C(γ, α)) : BoundedContinuousFunction.compContinuous 1 f = 1

instance BoundedContinuousFunction.instAdd {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] : Add (BoundedContinuousFunction α β)

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

Equations

• BoundedContinuousFunction.instAdd = { add := fun (f g : BoundedContinuousFunction α β) => { toFun := fun (x : α) => f x + g x, continuous_toFun := ⋯, map_bounded' := ⋯ } }

@[simp]

theorem BoundedContinuousFunction.coe_add {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) : ⇑(f + g) = ⇑f + ⇑g

theorem BoundedContinuousFunction.add_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) {x : α} : (f + g) x = f x + g x

@[simp]

theorem BoundedContinuousFunction.mkOfCompact_add {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] [CompactSpace α] (f : C(α, β)) (g : C(α, β)) : BoundedContinuousFunction.mkOfCompact (f + g) = BoundedContinuousFunction.mkOfCompact f + BoundedContinuousFunction.mkOfCompact g

theorem BoundedContinuousFunction.add_compContinuous {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) [TopologicalSpace γ] (h : C(γ, α)) : (g + f).compContinuous h = g.compContinuous h + f.compContinuous h

@[simp]

theorem BoundedContinuousFunction.coe_nsmulRec {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (f : BoundedContinuousFunction α β) (n : ℕ) : ⇑(nsmulRec n f) = n • ⇑f

instance BoundedContinuousFunction.instSMulNat {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] : SMul ℕ (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instSMulNat = { smul := fun (n : ℕ) (f : BoundedContinuousFunction α β) => { toContinuousMap := n • f.toContinuousMap, map_bounded' := ⋯ } }

@[simp]

theorem BoundedContinuousFunction.coe_nsmul {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (r : ℕ) (f : BoundedContinuousFunction α β) : ⇑(r • f) = r • ⇑f

@[simp]

theorem BoundedContinuousFunction.nsmul_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (r : ℕ) (f : BoundedContinuousFunction α β) (v : α) : (r • f) v = r • f v

instance BoundedContinuousFunction.instAddMonoid {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] : AddMonoid (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instAddMonoid = Function.Injective.addMonoid (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem BoundedContinuousFunction.coeFnAddHom_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] : ∀ (a : BoundedContinuousFunction α β) (a_1 : α), BoundedContinuousFunction.coeFnAddHom a a_1 = a a_1

def BoundedContinuousFunction.coeFnAddHom {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] : BoundedContinuousFunction α β →+ α → β

Coercion of a NormedAddGroupHom is an AddMonoidHom. Similar to AddMonoidHom.coeFn.

Equations

• BoundedContinuousFunction.coeFnAddHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.toContinuousMapAddHom_apply (α : Type u) (β : Type v) [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (self : BoundedContinuousFunction α β) : (BoundedContinuousFunction.toContinuousMapAddHom α β) self = self.toContinuousMap

def BoundedContinuousFunction.toContinuousMapAddHom (α : Type u) (β : Type v) [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] : BoundedContinuousFunction α β →+ C(α, β)

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

Equations

• BoundedContinuousFunction.toContinuousMapAddHom α β = { toFun := BoundedContinuousFunction.toContinuousMap, map_zero' := ⋯, map_add' := ⋯ }

theorem BoundedContinuousFunction.instAddAddCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [BoundedAdd β] [ContinuousAdd β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) : f + g = g + f

instance BoundedContinuousFunction.instAddAddCommMonoid {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [BoundedAdd β] [ContinuousAdd β] : AddCommMonoid (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instAddAddCommMonoid = AddCommMonoid.mk ⋯

instance BoundedContinuousFunction.instAddCommMonoid {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [BoundedAdd β] [ContinuousAdd β] : AddCommMonoid (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instAddCommMonoid = AddCommMonoid.mk ⋯

@[simp]

theorem BoundedContinuousFunction.coe_sum {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [BoundedAdd β] [ContinuousAdd β] {ι : Type u_2} (s : Finset ι) (f : ι → BoundedContinuousFunction α β) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

theorem BoundedContinuousFunction.sum_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [BoundedAdd β] [ContinuousAdd β] {ι : Type u_2} (s : Finset ι) (f : ι → BoundedContinuousFunction α β) (a : α) : (∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a

instance BoundedContinuousFunction.instLipschitzAdd {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] : LipschitzAdd (BoundedContinuousFunction α β)

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instSub {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Sub R] [BoundedSub R] [ContinuousSub R] : Sub (BoundedContinuousFunction α R)

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

Equations

• BoundedContinuousFunction.instSub = { sub := fun (f g : BoundedContinuousFunction α R) => { toFun := fun (x : α) => f x - g x, continuous_toFun := ⋯, map_bounded' := ⋯ } }

theorem BoundedContinuousFunction.sub_apply {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Sub R] [BoundedSub R] [ContinuousSub R] (f : BoundedContinuousFunction α R) (g : BoundedContinuousFunction α R) {x : α} : (f - g) x = f x - g x

@[simp]

theorem BoundedContinuousFunction.coe_sub {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Sub R] [BoundedSub R] [ContinuousSub R] (f : BoundedContinuousFunction α R) (g : BoundedContinuousFunction α R) : ⇑(f - g) = ⇑f - ⇑g

instance BoundedContinuousFunction.instNatCast {α : Type u} [TopologicalSpace α] {β : Type u_2} [PseudoMetricSpace β] [NatCast β] : NatCast (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instNatCast = { natCast := fun (n : ℕ) => BoundedContinuousFunction.const α ↑n }

@[simp]

theorem BoundedContinuousFunction.natCast_apply {α : Type u} [TopologicalSpace α] {β : Type u_2} [PseudoMetricSpace β] [NatCast β] (n : ℕ) (x : α) : ↑n x = ↑n

instance BoundedContinuousFunction.instIntCast {α : Type u} [TopologicalSpace α] {β : Type u_2} [PseudoMetricSpace β] [IntCast β] : IntCast (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instIntCast = { intCast := fun (m : ℤ) => BoundedContinuousFunction.const α ↑m }

@[simp]

theorem BoundedContinuousFunction.intCast_apply {α : Type u} [TopologicalSpace α] {β : Type u_2} [PseudoMetricSpace β] [IntCast β] (m : ℤ) (x : α) : ↑m x = ↑m

instance BoundedContinuousFunction.instMul {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Mul R] [BoundedMul R] [ContinuousMul R] : Mul (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instMul = { mul := fun (f g : BoundedContinuousFunction α R) => { toFun := fun (x : α) => f x * g x, continuous_toFun := ⋯, map_bounded' := ⋯ } }

@[simp]

theorem BoundedContinuousFunction.coe_mul {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Mul R] [BoundedMul R] [ContinuousMul R] (f : BoundedContinuousFunction α R) (g : BoundedContinuousFunction α R) : ⇑(f * g) = ⇑f * ⇑g

theorem BoundedContinuousFunction.mul_apply {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Mul R] [BoundedMul R] [ContinuousMul R] (f : BoundedContinuousFunction α R) (g : BoundedContinuousFunction α R) (x : α) : (f * g) x = f x * g x

instance BoundedContinuousFunction.instPow {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Monoid R] [BoundedMul R] [ContinuousMul R] : Pow (BoundedContinuousFunction α R) ℕ

Equations

• BoundedContinuousFunction.instPow = { pow := fun (f : BoundedContinuousFunction α R) (n : ℕ) => { toFun := fun (x : α) => f x ^ n, continuous_toFun := ⋯, map_bounded' := ⋯ } }

theorem BoundedContinuousFunction.coe_pow {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Monoid R] [BoundedMul R] [ContinuousMul R] (n : ℕ) (f : BoundedContinuousFunction α R) : ⇑(f ^ n) = ⇑f ^ n

@[simp]

theorem BoundedContinuousFunction.pow_apply {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Monoid R] [BoundedMul R] [ContinuousMul R] (n : ℕ) (f : BoundedContinuousFunction α R) (x : α) : (f ^ n) x = f x ^ n

instance BoundedContinuousFunction.instMonoid {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Monoid R] [BoundedMul R] [ContinuousMul R] : Monoid (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instMonoid = Function.Injective.monoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

instance BoundedContinuousFunction.instCommMonoid {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [CommMonoid R] [BoundedMul R] [ContinuousMul R] : CommMonoid (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instCommMonoid = CommMonoid.mk ⋯

instance BoundedContinuousFunction.instSemiring {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Semiring R] [BoundedMul R] [ContinuousMul R] [BoundedAdd R] [ContinuousAdd R] : Semiring (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instSemiring = Function.Injective.semiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance BoundedContinuousFunction.instNorm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] : Norm (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instNorm = { norm := fun (x : BoundedContinuousFunction α β) => dist x 0 }

theorem BoundedContinuousFunction.norm_def {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f‖ = dist f 0

theorem BoundedContinuousFunction.norm_eq {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f‖ = sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C}

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

theorem BoundedContinuousFunction.norm_eq_of_nonempty {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) [h : Nonempty α] : ‖f‖ = sInf {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 a sInf.

@[simp]

theorem BoundedContinuousFunction.norm_eq_zero_of_empty {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) [IsEmpty α] : ‖f‖ = 0

theorem BoundedContinuousFunction.norm_coe_le_norm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (x : α) : ‖f x‖ ≤ ‖f‖

theorem BoundedContinuousFunction.neg_norm_le_apply {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) (x : α) : -‖f‖ ≤ f x

theorem BoundedContinuousFunction.apply_le_norm {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) (x : α) : f x ≤ ‖f‖

theorem BoundedContinuousFunction.dist_le_two_norm' {β : Type v} {γ : Type w} [SeminormedAddCommGroup β] {f : γ → β} {C : ℝ} (hC : ∀ (x : γ), ‖f x‖ ≤ C) (x : γ) (y : γ) : dist (f x) (f y) ≤ 2 * C

theorem BoundedContinuousFunction.dist_le_two_norm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (x : α) (y : α) : dist (f x) (f y) ≤ 2 * ‖f‖

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

theorem BoundedContinuousFunction.norm_le {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] {f : BoundedContinuousFunction α β} {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 BoundedContinuousFunction.norm_le_of_nonempty {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [Nonempty α] {f : BoundedContinuousFunction α β} {M : ℝ} : ‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M

theorem BoundedContinuousFunction.norm_lt_iff_of_compact {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [CompactSpace α] {f : BoundedContinuousFunction α β} {M : ℝ} (M0 : 0 < M) : ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

theorem BoundedContinuousFunction.norm_lt_iff_of_nonempty_compact {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [Nonempty α] [CompactSpace α] {f : BoundedContinuousFunction α β} {M : ℝ} : ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

theorem BoundedContinuousFunction.norm_const_le {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (b : β) : ‖BoundedContinuousFunction.const α b‖ ≤ ‖b‖

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

@[simp]

theorem BoundedContinuousFunction.norm_const_eq {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [h : Nonempty α] (b : β) : ‖BoundedContinuousFunction.const α b‖ = ‖b‖

def BoundedContinuousFunction.ofNormedAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : α → β) (Hf : Continuous f) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) : BoundedContinuousFunction α β

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

Equations

• BoundedContinuousFunction.ofNormedAddCommGroup f Hf C H = { toFun := fun (n : α) => f n, continuous_toFun := Hf, map_bounded' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.coe_ofNormedAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : α → β) (Hf : Continuous f) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) : ⇑(BoundedContinuousFunction.ofNormedAddCommGroup f Hf C H) = f

theorem BoundedContinuousFunction.norm_ofNormedAddCommGroup_le {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] {f : α → β} (hfc : Continuous f) {C : ℝ} (hC : 0 ≤ C) (hfC : ∀ (x : α), ‖f x‖ ≤ C) : ‖BoundedContinuousFunction.ofNormedAddCommGroup f hfc C hfC‖ ≤ C

def BoundedContinuousFunction.ofNormedAddCommGroupDiscrete {α : Type u} {β : Type v} [TopologicalSpace α] [DiscreteTopology α] [SeminormedAddCommGroup β] (f : α → β) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) : BoundedContinuousFunction α β

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

Equations

• BoundedContinuousFunction.ofNormedAddCommGroupDiscrete f C H = BoundedContinuousFunction.ofNormedAddCommGroup f ⋯ C H

@[simp]

theorem BoundedContinuousFunction.coe_ofNormedAddCommGroupDiscrete {α : Type u} {β : Type v} [TopologicalSpace α] [DiscreteTopology α] [SeminormedAddCommGroup β] (f : α → β) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) : ⇑(BoundedContinuousFunction.ofNormedAddCommGroupDiscrete f C H) = f

def BoundedContinuousFunction.normComp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : BoundedContinuousFunction α ℝ

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

Equations

• f.normComp = BoundedContinuousFunction.comp norm ⋯ f

@[simp]

theorem BoundedContinuousFunction.coe_normComp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ⇑f.normComp = norm ∘ ⇑f

@[simp]

theorem BoundedContinuousFunction.norm_normComp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f.normComp‖ = ‖f‖

theorem BoundedContinuousFunction.bddAbove_range_norm_comp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : BddAbove (Set.range (norm ∘ ⇑f))

theorem BoundedContinuousFunction.norm_eq_iSup_norm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f‖ = ⨆ (x : α), ‖f x‖

instance BoundedContinuousFunction.instNormOneClass {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [Nonempty α] [One β] [NormOneClass β] : NormOneClass (BoundedContinuousFunction α β)

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

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instNeg {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] : Neg (BoundedContinuousFunction α β)

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

Equations

• BoundedContinuousFunction.instNeg = { neg := fun (f : BoundedContinuousFunction α β) => BoundedContinuousFunction.ofNormedAddCommGroup (-⇑f) ⋯ ‖f‖ ⋯ }

@[simp]

theorem BoundedContinuousFunction.coe_neg {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ⇑(-f) = -⇑f

theorem BoundedContinuousFunction.neg_apply {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) {x : α} : (-f) x = -f x

@[simp]

theorem BoundedContinuousFunction.mkOfCompact_neg {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [CompactSpace α] (f : C(α, β)) : BoundedContinuousFunction.mkOfCompact (-f) = -BoundedContinuousFunction.mkOfCompact f

@[simp]

theorem BoundedContinuousFunction.mkOfCompact_sub {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [CompactSpace α] (f : C(α, β)) (g : C(α, β)) : BoundedContinuousFunction.mkOfCompact (f - g) = BoundedContinuousFunction.mkOfCompact f - BoundedContinuousFunction.mkOfCompact g

@[simp]

theorem BoundedContinuousFunction.coe_zsmulRec {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (z : ℤ) : ⇑(zsmulRec (fun (x1 : ℕ) (x2 : BoundedContinuousFunction α β) => x1 • x2) z f) = z • ⇑f

instance BoundedContinuousFunction.instSMulInt {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] : SMul ℤ (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instSMulInt = { smul := fun (n : ℤ) (f : BoundedContinuousFunction α β) => { toContinuousMap := n • f.toContinuousMap, map_bounded' := ⋯ } }

@[simp]

theorem BoundedContinuousFunction.coe_zsmul {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (r : ℤ) (f : BoundedContinuousFunction α β) : ⇑(r • f) = r • ⇑f

@[simp]

theorem BoundedContinuousFunction.zsmul_apply {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (r : ℤ) (f : BoundedContinuousFunction α β) (v : α) : (r • f) v = r • f v

instance BoundedContinuousFunction.instAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] : AddCommGroup (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instAddCommGroup = Function.Injective.addCommGroup (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance BoundedContinuousFunction.instSeminormedAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] : SeminormedAddCommGroup (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯

instance BoundedContinuousFunction.instNormedAddCommGroup {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [NormedAddCommGroup β] : NormedAddCommGroup (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instNormedAddCommGroup = NormedAddCommGroup.mk ⋯

theorem BoundedContinuousFunction.nnnorm_def {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f‖₊ = nndist f 0

theorem BoundedContinuousFunction.nnnorm_coe_le_nnnorm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (x : α) : ‖f x‖₊ ≤ ‖f‖₊

theorem BoundedContinuousFunction.nndist_le_two_nnnorm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (x : α) (y : α) : nndist (f x) (f y) ≤ 2 * ‖f‖₊

theorem BoundedContinuousFunction.nnnorm_le {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (C : NNReal) : ‖f‖₊ ≤ C ↔ ∀ (x : α), ‖f x‖₊ ≤ C

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

theorem BoundedContinuousFunction.nnnorm_const_le {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (b : β) : ‖BoundedContinuousFunction.const α b‖₊ ≤ ‖b‖₊

@[simp]

theorem BoundedContinuousFunction.nnnorm_const_eq {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [Nonempty α] (b : β) : ‖BoundedContinuousFunction.const α b‖₊ = ‖b‖₊

theorem BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f‖₊ = ⨆ (x : α), ‖f x‖₊

theorem BoundedContinuousFunction.abs_diff_coe_le_dist {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) {x : α} : ‖f x - g x‖ ≤ dist f g

theorem BoundedContinuousFunction.coe_le_coe_add_dist {α : Type u} [TopologicalSpace α] {x : α} {f : BoundedContinuousFunction α ℝ} {g : BoundedContinuousFunction α ℝ} : f x ≤ g x + dist f g

theorem BoundedContinuousFunction.norm_compContinuous_le {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [SeminormedAddCommGroup β] [TopologicalSpace γ] (f : BoundedContinuousFunction α β) (g : C(γ, α)) : ‖f.compContinuous g‖ ≤ ‖f‖

BoundedSMul (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 BoundedSMul structure (in particular, a ContinuousMul structure, which is the mathlib formulation of being a topological module), by using pointwise operations and checking that they are compatible with the uniform distance.

instance BoundedContinuousFunction.instSMul {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] : SMul 𝕜 (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instSMul = { smul := fun (c : 𝕜) (f : BoundedContinuousFunction α β) => { toContinuousMap := c • f.toContinuousMap, map_bounded' := ⋯ } }

@[simp]

theorem BoundedContinuousFunction.coe_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] (c : 𝕜) (f : BoundedContinuousFunction α β) : ⇑(c • f) = fun (x : α) => c • f x

theorem BoundedContinuousFunction.smul_apply {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] (c : 𝕜) (f : BoundedContinuousFunction α β) (x : α) : (c • f) x = c • f x

instance BoundedContinuousFunction.instIsScalarTower {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] {𝕜' : Type u_3} [PseudoMetricSpace 𝕜'] [Zero 𝕜'] [SMul 𝕜' β] [BoundedSMul 𝕜' β] [SMul 𝕜' 𝕜] [IsScalarTower 𝕜' 𝕜 β] : IsScalarTower 𝕜' 𝕜 (BoundedContinuousFunction α β)

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instSMulCommClass {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] {𝕜' : Type u_3} [PseudoMetricSpace 𝕜'] [Zero 𝕜'] [SMul 𝕜' β] [BoundedSMul 𝕜' β] [SMulCommClass 𝕜' 𝕜 β] : SMulCommClass 𝕜' 𝕜 (BoundedContinuousFunction α β)

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instIsCentralScalar {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] [SMul 𝕜ᵐᵒᵖ β] [IsCentralScalar 𝕜 β] : IsCentralScalar 𝕜 (BoundedContinuousFunction α β)

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instBoundedSMul {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] : BoundedSMul 𝕜 (BoundedContinuousFunction α β)

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instMulAction {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [MonoidWithZero 𝕜] [Zero β] [MulAction 𝕜 β] [BoundedSMul 𝕜 β] : MulAction 𝕜 (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instMulAction = Function.Injective.mulAction (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯

instance BoundedContinuousFunction.instDistribMulAction {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [MonoidWithZero 𝕜] [AddMonoid β] [DistribMulAction 𝕜 β] [BoundedSMul 𝕜 β] [BoundedAdd β] [ContinuousAdd β] : DistribMulAction 𝕜 (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instDistribMulAction = Function.Injective.distribMulAction { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance BoundedContinuousFunction.instModule {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Semiring 𝕜] [AddCommMonoid β] [Module 𝕜 β] [BoundedSMul 𝕜 β] [BoundedAdd β] [ContinuousAdd β] : Module 𝕜 (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instModule = Function.Injective.module 𝕜 { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

def BoundedContinuousFunction.evalCLM {α : Type u} {β : Type v} (𝕜 : Type u_2) [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Semiring 𝕜] [AddCommMonoid β] [Module 𝕜 β] [BoundedSMul 𝕜 β] [BoundedAdd β] [ContinuousAdd β] (x : α) : BoundedContinuousFunction α β →L[𝕜] β

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

Equations

• BoundedContinuousFunction.evalCLM 𝕜 x = { toFun := fun (f : BoundedContinuousFunction α β) => f x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem BoundedContinuousFunction.evalCLM_apply {α : Type u} {β : Type v} (𝕜 : Type u_2) [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Semiring 𝕜] [AddCommMonoid β] [Module 𝕜 β] [BoundedSMul 𝕜 β] [BoundedAdd β] [ContinuousAdd β] (x : α) (f : BoundedContinuousFunction α β) : (BoundedContinuousFunction.evalCLM 𝕜 x) f = f x

@[simp]

theorem BoundedContinuousFunction.toContinuousMapLinearMap_apply (α : Type u) (β : Type v) (𝕜 : Type u_2) [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Semiring 𝕜] [AddCommMonoid β] [Module 𝕜 β] [BoundedSMul 𝕜 β] [BoundedAdd β] [ContinuousAdd β] (self : BoundedContinuousFunction α β) : (BoundedContinuousFunction.toContinuousMapLinearMap α β 𝕜) self = self.toContinuousMap

def BoundedContinuousFunction.toContinuousMapLinearMap (α : Type u) (β : Type v) (𝕜 : Type u_2) [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Semiring 𝕜] [AddCommMonoid β] [Module 𝕜 β] [BoundedSMul 𝕜 β] [BoundedAdd β] [ContinuousAdd β] : BoundedContinuousFunction α β →ₗ[𝕜] C(α, β)

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

Equations

• BoundedContinuousFunction.toContinuousMapLinearMap α β 𝕜 = { toFun := BoundedContinuousFunction.toContinuousMap, map_add' := ⋯, map_smul' := ⋯ }

Normed space structure

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

instance BoundedContinuousFunction.instNormedSpace {α : Type u} {β : Type v} {𝕜 : Type u_2} [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedField 𝕜] [NormedSpace 𝕜 β] : NormedSpace 𝕜 (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instNormedSpace = NormedSpace.mk ⋯

def ContinuousLinearMap.compLeftContinuousBounded (α : Type u) {β : Type v} {γ : Type w} {𝕜 : Type u_2} [TopologicalSpace α] [SeminormedAddCommGroup β] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 β] [SeminormedAddCommGroup γ] [NormedSpace 𝕜 γ] (g : β →L[𝕜] γ) : BoundedContinuousFunction α β →L[𝕜] BoundedContinuousFunction α γ

Postcomposition of bounded continuous functions into a normed module by a continuous linear map is a continuous linear map. Upgraded version of ContinuousLinearMap.compLeftContinuous, similar to LinearMap.compLeft.

Equations

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

@[simp]

theorem ContinuousLinearMap.compLeftContinuousBounded_apply (α : Type u) {β : Type v} {γ : Type w} {𝕜 : Type u_2} [TopologicalSpace α] [SeminormedAddCommGroup β] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 β] [SeminormedAddCommGroup γ] [NormedSpace 𝕜 γ] (g : β →L[𝕜] γ) (f : BoundedContinuousFunction α β) (x : α) : ((ContinuousLinearMap.compLeftContinuousBounded α 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.

instance BoundedContinuousFunction.instNonUnitalRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [NonUnitalSeminormedRing R] : NonUnitalRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instNonUnitalRing = Function.Injective.nonUnitalRing (fun (f : BoundedContinuousFunction α R) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance BoundedContinuousFunction.instNonUnitalSeminormedRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [NonUnitalSeminormedRing R] : NonUnitalSeminormedRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

instance BoundedContinuousFunction.instNonUnitalSeminormedCommRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [NonUnitalSeminormedCommRing R] : NonUnitalSeminormedCommRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instNonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

instance BoundedContinuousFunction.instNonUnitalNormedRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [NonUnitalNormedRing R] : NonUnitalNormedRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

instance BoundedContinuousFunction.instNonUnitalNormedCommRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [NonUnitalNormedCommRing R] : NonUnitalNormedCommRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instNonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

@[simp]

theorem BoundedContinuousFunction.coe_npowRec {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] (f : BoundedContinuousFunction α R) (n : ℕ) : ⇑(npowRec n f) = ⇑f ^ n

instance BoundedContinuousFunction.hasNatPow {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] : Pow (BoundedContinuousFunction α R) ℕ

Equations

• BoundedContinuousFunction.hasNatPow = { pow := fun (f : BoundedContinuousFunction α R) (n : ℕ) => { toContinuousMap := f.toContinuousMap ^ n, map_bounded' := ⋯ } }

instance BoundedContinuousFunction.instNatCast_1 {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] : NatCast (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instNatCast_1 = { natCast := fun (n : ℕ) => BoundedContinuousFunction.const α ↑n }

@[simp]

theorem BoundedContinuousFunction.coe_natCast {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] (n : ℕ) : ⇑↑n = ↑n

@[simp]

theorem BoundedContinuousFunction.coe_ofNat {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] (n : ℕ) [n.AtLeastTwo] : ⇑(OfNat.ofNat n) = OfNat.ofNat n

instance BoundedContinuousFunction.instIntCast_1 {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] : IntCast (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instIntCast_1 = { intCast := fun (n : ℤ) => BoundedContinuousFunction.const α ↑n }

@[simp]

theorem BoundedContinuousFunction.coe_intCast {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] (n : ℤ) : ⇑↑n = ↑n

instance BoundedContinuousFunction.instRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] : Ring (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instRing = Function.Injective.ring (fun (f : BoundedContinuousFunction α R) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance BoundedContinuousFunction.instSeminormedRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] : SeminormedRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instSeminormedRing = SeminormedRing.mk ⋯ ⋯

instance BoundedContinuousFunction.instNormedRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [NormedRing R] : NormedRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instNormedRing = NormedRing.mk ⋯ ⋯

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.

instance BoundedContinuousFunction.instCommRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedCommRing R] : CommRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instCommRing = CommRing.mk ⋯

instance BoundedContinuousFunction.instSeminormedCommRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedCommRing R] : SeminormedCommRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instSeminormedCommRing = SeminormedCommRing.mk ⋯

instance BoundedContinuousFunction.instNormedCommRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [NormedCommRing R] : NormedCommRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instNormedCommRing = NormedCommRing.mk ⋯

instance BoundedContinuousFunction.instIsScalarTower_1 {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [NonUnitalSeminormedRing β] [Zero 𝕜] [SMul 𝕜 β] [BoundedSMul 𝕜 β] [IsScalarTower 𝕜 β β] : IsScalarTower 𝕜 (BoundedContinuousFunction α β) (BoundedContinuousFunction α β)

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instSMulCommClass_1 {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [NonUnitalSeminormedRing β] [Zero 𝕜] [SMul 𝕜 β] [BoundedSMul 𝕜 β] [SMulCommClass 𝕜 β β] : SMulCommClass 𝕜 (BoundedContinuousFunction α β) (BoundedContinuousFunction α β)

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instSMulCommClass_2 {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [NonUnitalSeminormedRing β] [Zero 𝕜] [SMul 𝕜 β] [BoundedSMul 𝕜 β] [SMulCommClass 𝕜 β β] : SMulCommClass (BoundedContinuousFunction α β) 𝕜 (BoundedContinuousFunction α β)

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 BoundedContinuousFunction.C {α : Type u} {γ : Type w} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] : 𝕜 →+* BoundedContinuousFunction α γ

BoundedContinuousFunction.const as a RingHom.

Equations

• BoundedContinuousFunction.C = { toFun := fun (c : 𝕜) => BoundedContinuousFunction.const α ((algebraMap 𝕜 γ) c), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

instance BoundedContinuousFunction.instAlgebra {α : Type u} {γ : Type w} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] : Algebra 𝕜 (BoundedContinuousFunction α γ)

Equations

• BoundedContinuousFunction.instAlgebra = Algebra.mk BoundedContinuousFunction.C ⋯ ⋯

@[simp]

theorem BoundedContinuousFunction.algebraMap_apply {α : Type u} {γ : Type w} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] (k : 𝕜) (a : α) : ((algebraMap 𝕜 (BoundedContinuousFunction α γ)) k) a = k • 1

instance BoundedContinuousFunction.instNormedAlgebra {α : Type u} {γ : Type w} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] : NormedAlgebra 𝕜 (BoundedContinuousFunction α γ)

Equations

• BoundedContinuousFunction.instNormedAlgebra = NormedAlgebra.mk ⋯

Structure as normed module over scalar functions

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

instance BoundedContinuousFunction.instSMul' {α : Type u} {β : Type v} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedSpace 𝕜 β] : SMul (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)

Equations

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

instance BoundedContinuousFunction.instModule' {α : Type u} {β : Type v} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedSpace 𝕜 β] : Module (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instModule' = Module.ofMinimalAxioms ⋯ ⋯ ⋯ ⋯

instance BoundedContinuousFunction.instBoundedSMul_1 {α : Type u} {β : Type v} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedSpace 𝕜 β] : BoundedSMul (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)

Equations

• ⋯ = ⋯

theorem BoundedContinuousFunction.NNReal.upper_bound {α : Type u_2} [TopologicalSpace α] (f : BoundedContinuousFunction α NNReal) (x : α) : f x ≤ 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 BoundedContinuousFunction.complete).

instance BoundedContinuousFunction.instStarAddMonoid {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] : StarAddMonoid (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instStarAddMonoid = StarAddMonoid.mk ⋯

@[simp]

theorem BoundedContinuousFunction.coe_star {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] (f : BoundedContinuousFunction α β) : ⇑(star f) = star ⇑f

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

@[simp]

theorem BoundedContinuousFunction.star_apply {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] (f : BoundedContinuousFunction α β) (x : α) : (star f) x = star (f x)

instance BoundedContinuousFunction.instNormedStarGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] : NormedStarGroup (BoundedContinuousFunction α β)

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instStarModule {α : Type u} {β : Type v} {𝕜 : Type u_2} [NormedField 𝕜] [StarRing 𝕜] [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] [NormedSpace 𝕜 β] [StarModule 𝕜 β] : StarModule 𝕜 (BoundedContinuousFunction α β)

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instStarRing {α : Type u} {β : Type v} [TopologicalSpace α] [NonUnitalNormedRing β] [StarRing β] [NormedStarGroup β] : StarRing (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instStarRing = StarRing.mk ⋯

instance BoundedContinuousFunction.instCStarRing {α : Type u} {β : Type v} [TopologicalSpace α] [NonUnitalNormedRing β] [StarRing β] [CStarRing β] : CStarRing (BoundedContinuousFunction α β)

Equations

• ⋯ = ⋯

instance BoundedContinuousFunction.instPartialOrder {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] : PartialOrder (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instPartialOrder = PartialOrder.lift (fun (f : BoundedContinuousFunction α β) => f.toFun) ⋯

instance BoundedContinuousFunction.instSup {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] : Sup (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instSup = { sup := fun (f g : BoundedContinuousFunction α β) => { toFun := ⇑f ⊔ ⇑g, continuous_toFun := ⋯, map_bounded' := ⋯ } }

instance BoundedContinuousFunction.instInf {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] : Inf (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instInf = { inf := fun (f g : BoundedContinuousFunction α β) => { toFun := ⇑f ⊓ ⇑g, continuous_toFun := ⋯, map_bounded' := ⋯ } }

@[simp]

theorem BoundedContinuousFunction.coe_sup {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) : ⇑(f ⊔ g) = ⇑f ⊔ ⇑g

@[simp]

theorem BoundedContinuousFunction.coe_inf {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) : ⇑(f ⊓ g) = ⇑f ⊓ ⇑g

instance BoundedContinuousFunction.instSemilatticeSup {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] : SemilatticeSup (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯

instance BoundedContinuousFunction.instSemilatticeInf {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] : SemilatticeInf (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instSemilatticeInf = Function.Injective.semilatticeInf (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯

instance BoundedContinuousFunction.instLattice {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] : Lattice (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instLattice = Function.Injective.lattice (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯ ⋯

@[simp]

theorem BoundedContinuousFunction.coe_abs {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] (f : BoundedContinuousFunction α β) : ⇑|f| = |⇑f|

@[simp]

theorem BoundedContinuousFunction.coe_posPart {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] (f : BoundedContinuousFunction α β) : ⇑f⁺ = (⇑f)⁺

@[simp]

theorem BoundedContinuousFunction.coe_negPart {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] (f : BoundedContinuousFunction α β) : ⇑f⁻ = (⇑f)⁻

@[deprecated BoundedContinuousFunction.coe_sup]

theorem BoundedContinuousFunction.coeFn_sup {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) : ⇑(f ⊔ g) = ⇑f ⊔ ⇑g

Alias of BoundedContinuousFunction.coe_sup.

@[deprecated BoundedContinuousFunction.coe_abs]

theorem BoundedContinuousFunction.coeFn_abs {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] (f : BoundedContinuousFunction α β) : ⇑|f| = |⇑f|

Alias of BoundedContinuousFunction.coe_abs.

instance BoundedContinuousFunction.instNormedLatticeAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [NormedLatticeAddCommGroup β] : NormedLatticeAddCommGroup (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instNormedLatticeAddCommGroup = NormedLatticeAddCommGroup.mk ⋯

def BoundedContinuousFunction.nnrealPart {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : BoundedContinuousFunction α NNReal

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

Equations

• f.nnrealPart = BoundedContinuousFunction.comp Real.toNNReal BoundedContinuousFunction.nnrealPart.proof_1 f

@[simp]

theorem BoundedContinuousFunction.nnrealPart_coeFn_eq {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : ⇑f.nnrealPart = Real.toNNReal ∘ ⇑f

def BoundedContinuousFunction.nnnorm {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : BoundedContinuousFunction α NNReal

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

Equations

• f.nnnorm = BoundedContinuousFunction.comp (fun (x : ℝ) => ‖x‖₊) BoundedContinuousFunction.nnnorm.proof_1 f

@[simp]

theorem BoundedContinuousFunction.nnnorm_coeFn_eq {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : ⇑f.nnnorm = nnnorm ∘ ⇑f

theorem BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : ⇑f = NNReal.toReal ∘ ⇑f.nnrealPart - NNReal.toReal ∘ ⇑(-f).nnrealPart

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

theorem BoundedContinuousFunction.abs_self_eq_nnrealPart_add_nnrealPart_neg {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : abs ∘ ⇑f = NNReal.toReal ∘ ⇑f.nnrealPart + NNReal.toReal ∘ ⇑(-f).nnrealPart

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

theorem BoundedContinuousFunction.add_norm_nonneg {α : Type u_2} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : 0 ≤ f + BoundedContinuousFunction.const α ‖f‖

theorem BoundedContinuousFunction.norm_sub_nonneg {α : Type u_2} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : 0 ≤ BoundedContinuousFunction.const α ‖f‖ - f