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)

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

α →ᵇ β 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.

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 β] extends ContinuousMapClass : Type (max (max u_2 u_3) u_4)

• coe : F → α → β
• coe_injective' : Function.Injective FunLike.coe
• map_continuous : ∀ (f : F), Continuous ↑f
• map_bounded : ∀ (f : F), ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C

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

You should also extend this typeclass when you extend BoundedContinuousFunction.

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

Equations

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

instance BoundedContinuousFunction.instCoeFunBoundedContinuousFunctionForAll {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : CoeFun (BoundedContinuousFunction α β) fun x => α → β

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun directly.

Equations

• BoundedContinuousFunction.instCoeFunBoundedContinuousFunctionForAll = FunLike.hasCoeToFun

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

Equations

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

@[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 {α : 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' := (_ : ∃ C, ∀ (x y : α), dist (ContinuousMap.toFun f x) (ContinuousMap.toFun f y) ≤ C) }

@[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' := (_ : ∃ C, ∀ (x y : α), dist (ContinuousMap.toFun f x) (ContinuousMap.toFun f y) ≤ C) }

@[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_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

@[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

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

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

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

The uniform distance between two bounded continuous functions.

Equations

• BoundedContinuousFunction.instDistBoundedContinuousFunction = { dist := fun f g => 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.instPseudoMetricSpaceBoundedContinuousFunction {α : 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.instMetricSpaceBoundedContinuousFunctionToPseudoMetricSpace {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [MetricSpace β] : MetricSpace (BoundedContinuousFunction α β)

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

Equations

• BoundedContinuousFunction.instMetricSpaceBoundedContinuousFunctionToPseudoMetricSpace = MetricSpace.mk (_ : ∀ {x y : BoundedContinuousFunction α β}, dist x y = 0 → x = y)

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

theorem BoundedContinuousFunction.nndist_set_exists {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} : ∃ C, ∀ (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.inducing_coeFn {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : Inducing (↑UniformFun.ofFun ∘ FunLike.coe)

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

theorem BoundedContinuousFunction.embedding_coeFn {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : Embedding (↑UniformFun.ofFun ∘ FunLike.coe)

@[simp]

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

@[simp]

theorem BoundedContinuousFunction.const_apply (α : 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

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

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

instance BoundedContinuousFunction.instInhabitedBoundedContinuousFunction {α : 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.instInhabitedBoundedContinuousFunction = { default := BoundedContinuousFunction.const α default }

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

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

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

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

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

theorem BoundedContinuousFunction.continuous_eval {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] : Continuous fun p => ↑p.fst p.snd

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

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

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

Equations

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

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

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

@[simp]

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

@[simp]

theorem BoundedContinuousFunction.compContinuous_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] (f : BoundedContinuousFunction α β) (g : C(δ, α)) (x : δ) : ↑(BoundedContinuousFunction.compContinuous f 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.compContinuous f g

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

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

@[simp]

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

@[simp]

theorem BoundedContinuousFunction.restrict_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) (s : Set α) (x : ↑s) : ↑(BoundedContinuousFunction.restrict f 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

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

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 = { toContinuousMap := ContinuousMap.mk (Set.codRestrict (↑f) s H), map_bounded' := (_ : ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C) }

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

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

@[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 (BoundedContinuousFunction.restrict h₁ (Set.range ↑f)ᶜ) (BoundedContinuousFunction.restrict h₂ (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.extend f g h

theorem BoundedContinuousFunction.arzela_ascoli₁ {α : Type u} {β : Type v} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] [CompactSpace β] (A : Set (BoundedContinuousFunction α β)) (closed : IsClosed A) (H : Equicontinuous fun x => ↑↑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 => ↑↑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 => ↑↑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.instZeroBoundedContinuousFunction {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] : Zero (BoundedContinuousFunction α β)

Equations

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

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

Equations

• BoundedContinuousFunction.instOneBoundedContinuousFunction = { 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.instAddBoundedContinuousFunction {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] : Add (BoundedContinuousFunction α β)

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

Equations

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

@[simp]

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

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

@[simp]

theorem BoundedContinuousFunction.mkOfCompact_add {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] [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 β] [LipschitzAdd β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) [TopologicalSpace γ] (h : C(γ, α)) : BoundedContinuousFunction.compContinuous (g + f) h = BoundedContinuousFunction.compContinuous g h + BoundedContinuousFunction.compContinuous f h

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

@[simp]

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

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

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

Equations

• BoundedContinuousFunction.coeFnAddHom = { toZeroHom := { toFun := FunLike.coe, map_zero' := (_ : ↑0 = 0) }, map_add' := (_ : ∀ (f g : BoundedContinuousFunction α β), ↑(f + g) = ↑f + ↑g) }

@[simp]

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

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

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

Equations

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

theorem BoundedContinuousFunction.instAddAddCommMonoidBoundedContinuousFunction.proof_3 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [LipschitzAdd β] (x : BoundedContinuousFunction α β) : AddMonoid.nsmul 0 x = 0

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

Equations

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

theorem BoundedContinuousFunction.instAddAddCommMonoidBoundedContinuousFunction.proof_2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [LipschitzAdd β] (a : BoundedContinuousFunction α β) : a + 0 = a

theorem BoundedContinuousFunction.instAddAddCommMonoidBoundedContinuousFunction.proof_5 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [LipschitzAdd β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) : f + g = g + f

theorem BoundedContinuousFunction.instAddAddCommMonoidBoundedContinuousFunction.proof_4 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [LipschitzAdd β] (n : ℕ) (x : BoundedContinuousFunction α β) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

theorem BoundedContinuousFunction.instAddAddCommMonoidBoundedContinuousFunction.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [LipschitzAdd β] (a : BoundedContinuousFunction α β) : 0 + a = a

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

Equations

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

@[simp]

theorem BoundedContinuousFunction.coe_sum {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [LipschitzAdd β] {ι : Type u_2} (s : Finset ι) (f : ι → BoundedContinuousFunction α β) : ↑(Finset.sum s fun i => f i) = Finset.sum s fun i => ↑(f i)

theorem BoundedContinuousFunction.sum_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [LipschitzAdd β] {ι : Type u_2} (s : Finset ι) (f : ι → BoundedContinuousFunction α β) (a : α) : ↑(Finset.sum s fun i => f i) a = Finset.sum s fun i => ↑(f i) a

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

Equations

• BoundedContinuousFunction.instNormBoundedContinuousFunctionToPseudoMetricSpace = { norm := fun u => dist u 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

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

@[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 (_ : Continuous 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

• BoundedContinuousFunction.normComp f = BoundedContinuousFunction.comp norm (_ : LipschitzWith 1 norm) f

@[simp]

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

@[simp]

theorem BoundedContinuousFunction.norm_normComp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖BoundedContinuousFunction.normComp f‖ = ‖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.instNormOneClassBoundedContinuousFunctionToPseudoMetricSpaceInstNormBoundedContinuousFunctionToPseudoMetricSpaceInstOneBoundedContinuousFunction {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [Nonempty α] [One β] [NormOneClass β] : NormOneClass (BoundedContinuousFunction α β)

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

Equations

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

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

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

Equations

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

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

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

Equations

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

@[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.coe_sub {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) : ↑(f - g) = ↑f - ↑g

theorem BoundedContinuousFunction.sub_apply {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) {x : α} : ↑(f - g) x = ↑f x - ↑g 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 z f) = z • ↑f

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

Equations

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

@[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.instAddCommGroupBoundedContinuousFunctionToPseudoMetricSpace {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] : AddCommGroup (BoundedContinuousFunction α β)

Equations

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

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

Equations

• BoundedContinuousFunction.seminormedAddCommGroup = SeminormedAddCommGroup.mk

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

Equations

• BoundedContinuousFunction.normedAddCommGroup = let src := BoundedContinuousFunction.seminormedAddCommGroup; 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(γ, α)) : ‖BoundedContinuousFunction.compContinuous f 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.instSMulBoundedContinuousFunction {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] : SMul 𝕜 (BoundedContinuousFunction α β)

Equations

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

@[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.instIsCentralScalarBoundedContinuousFunctionInstSMulBoundedContinuousFunctionMulOppositeInstPseudoMetricSpaceMulOppositeZeroOp {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] [SMul 𝕜ᵐᵒᵖ β] [IsCentralScalar 𝕜 β] : IsCentralScalar 𝕜 (BoundedContinuousFunction α β)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

@[simp]

theorem BoundedContinuousFunction.evalClm_apply {α : Type u} {β : Type v} (𝕜 : Type u_2) [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Semiring 𝕜] [AddCommMonoid β] [Module 𝕜 β] [BoundedSMul 𝕜 β] [LipschitzAdd β] (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 𝕜 β] [LipschitzAdd β] (self : BoundedContinuousFunction α β) : ↑(BoundedContinuousFunction.toContinuousMapLinearMap α β 𝕜) self = self.toContinuousMap

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

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

Equations

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

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.normedSpace {α : Type u} {β : Type v} {𝕜 : Type u_2} [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedField 𝕜] [NormedSpace 𝕜 β] : NormedSpace 𝕜 (BoundedContinuousFunction α β)

Equations

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

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.instMulBoundedContinuousFunctionToPseudoMetricSpace {α : Type u} [TopologicalSpace α] {R : Type u_2} [NonUnitalSeminormedRing R] : Mul (BoundedContinuousFunction α R)

Equations

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

@[simp]

theorem BoundedContinuousFunction.coe_mul {α : Type u} [TopologicalSpace α] {R : Type u_2} [NonUnitalSeminormedRing R] (f : BoundedContinuousFunction α R) (g : BoundedContinuousFunction α R) : ↑(f * g) = ↑f * ↑g

theorem BoundedContinuousFunction.mul_apply {α : Type u} [TopologicalSpace α] {R : Type u_2} [NonUnitalSeminormedRing R] (f : BoundedContinuousFunction α R) (g : BoundedContinuousFunction α R) (x : α) : ↑(f * g) x = ↑f x * ↑g x

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

Equations

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

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

Equations

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

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

Equations

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

@[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

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

@[simp]

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

@[simp]

theorem BoundedContinuousFunction.pow_apply {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] (n : ℕ) (f : BoundedContinuousFunction α R) (v : α) : ↑(f ^ n) v = ↑f v ^ n

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

Equations

• BoundedContinuousFunction.instNatCastBoundedContinuousFunctionToPseudoMetricSpace = { natCast := fun n => BoundedContinuousFunction.const α ↑n }

@[simp]

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

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

Equations

• BoundedContinuousFunction.instIntCastBoundedContinuousFunctionToPseudoMetricSpace = { 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.ring {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] : Ring (BoundedContinuousFunction α R)

Equations

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

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

Equations

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

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

Equations

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

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.commRing {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedCommRing R] : CommRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.commRing = let src := BoundedContinuousFunction.ring; CommRing.mk (_ : ∀ (x x_1 : BoundedContinuousFunction α R), x * x_1 = x_1 * x)

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

Equations

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

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

Equations

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

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

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

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

Equations

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

@[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.instNormedAlgebraBoundedContinuousFunctionToPseudoMetricSpaceToSeminormedRingInstSeminormedRingBoundedContinuousFunctionToPseudoMetricSpace {α : Type u} {γ : Type w} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] : NormedAlgebra 𝕜 (BoundedContinuousFunction α γ)

Equations

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

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.hasSmul' {α : 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.module' {α : Type u} {β : Type v} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedSpace 𝕜 β] : Module (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)

Equations

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

theorem BoundedContinuousFunction.norm_smul_le {α : Type u} {β : Type v} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedSpace 𝕜 β] (f : BoundedContinuousFunction α 𝕜) (g : BoundedContinuousFunction α β) : ‖f • g‖ ≤ ‖f‖ * ‖g‖

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.starAddMonoid {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] : StarAddMonoid (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.starAddMonoid = StarAddMonoid.mk (_ : ∀ (f g : BoundedContinuousFunction α β), star (f + g) = star f + star g)

@[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.instNormedStarGroupBoundedContinuousFunctionToPseudoMetricSpaceSeminormedAddCommGroupStarAddMonoid {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] : NormedStarGroup (BoundedContinuousFunction α β)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• BoundedContinuousFunction.partialOrder = PartialOrder.lift (fun f => f.toFun) (_ : ∀ (a a_1 : BoundedContinuousFunction α β), ↑a = ↑a_1 → a = a_1)

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

Continuous normed lattice group valued functions form a meet-semilattice.

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

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

@[simp]

theorem BoundedContinuousFunction.nnrealPart_coeFn_eq {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : ↑(BoundedContinuousFunction.nnrealPart f) = 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

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

@[simp]

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

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

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 ∘ ↑(BoundedContinuousFunction.nnrealPart f) + NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnrealPart (-f))

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