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 C(α, β) : 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

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

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

class BoundedContinuousMapClass (F : Type u_2) (α : outParam (Type u_3)) (β : outParam (Type u_4)) [TopologicalSpace α] [PseudoMetricSpace β] [FunLike F α β] extends ContinuousMapClass F α β : 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

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

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

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

@[simp]

theorem BoundedContinuousFunction.coe_toContinuousMap {α : 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.

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 g : BoundedContinuousFunction α β} (h : ∀ (x : α), f x = g x) : f = g

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

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

@[simp]

theorem BoundedContinuousFunction.mkOfBound_coe {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : C(α, β)} {C : ℝ} {h : ∀ (x y : α), dist (f x) (f y) ≤ C} : ⇑(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.

@[simp]

theorem BoundedContinuousFunction.mkOfCompact_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [CompactSpace α] (f : C(α, β)) (a : α) : (mkOfCompact f) 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.

@[simp]

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

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

The uniform distance between two bounded continuous functions.

theorem BoundedContinuousFunction.dist_eq {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f 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 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 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 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 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 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 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 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.

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.

theorem BoundedContinuousFunction.nndist_eq {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f 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 g : BoundedContinuousFunction α β} : ∃ (C : NNReal), ∀ (x : α), nndist (f x) (g x) ≤ C

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

theorem BoundedContinuousFunction.dist_zero_of_empty {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f 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 g : BoundedContinuousFunction α β} : dist f g = ⨆ (x : α), dist (f x) (g x)

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

theorem BoundedContinuousFunction.edist_eq_iSup {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f g : BoundedContinuousFunction α β} : edist f g = ⨆ (x : α), edist (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 β] : Topology.IsInducing (⇑UniformFun.ofFun ∘ DFunLike.coe)

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

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

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

Constant as a continuous bounded function.

@[simp]

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

theorem BoundedContinuousFunction.const_apply' {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (a : α) (b : β) : (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.

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.

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.

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

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

@[simp]

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

theorem BoundedContinuousFunction.lipschitz_comp {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] {G : β → γ} {C : NNReal} (H : LipschitzWith C G) : LipschitzWith C (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 (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 (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.

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.

@[simp]

theorem BoundedContinuousFunction.extend_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] [DiscreteTopology δ] (f : α ↪ δ) (g : BoundedContinuousFunction α β) (h : BoundedContinuousFunction δ β) (x : α) : (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 δ β) : ⇑(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 δ β) : (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 δ β) : extend f g h = h

@[simp]

theorem BoundedContinuousFunction.dist_extend_extend {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] [DiscreteTopology δ] (f : α ↪ δ) (g₁ g₂ : BoundedContinuousFunction α β) (h₁ h₂ : BoundedContinuousFunction δ β) : dist (extend f g₁ h₁) (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 α β) => extend f g h

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.

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

instance BoundedContinuousFunction.instAdd {α : Type u} {R : Type u_2} [TopologicalSpace α] [PseudoMetricSpace R] [Add R] [BoundedAdd R] [ContinuousAdd R] : Add (BoundedContinuousFunction α R)

@[simp]

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

@[simp]

theorem BoundedContinuousFunction.coe_add {α : Type u} {R : Type u_2} [TopologicalSpace α] [PseudoMetricSpace R] [Add R] [BoundedAdd R] [ContinuousAdd R] (f g : BoundedContinuousFunction α R) : ⇑(f + g) = ⇑f + ⇑g

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

theorem BoundedContinuousFunction.add_apply {α : Type u} {R : Type u_2} [TopologicalSpace α] [PseudoMetricSpace R] [Add R] [BoundedAdd R] [ContinuousAdd R] (f g : BoundedContinuousFunction α R) (x : α) : (f + g) x = f x + g x

@[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 α β)

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

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

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

@[simp]

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

@[simp]

theorem BoundedContinuousFunction.nsmul_apply {α : Type u} {R : Type u_2} [TopologicalSpace α] [PseudoMetricSpace R] [AddMonoid R] [BoundedAdd R] [ContinuousAdd R] (n : ℕ) (f : BoundedContinuousFunction α R) (x : α) : (n • f) x = n • f x

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

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

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

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

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

instance BoundedContinuousFunction.instAddZeroClass {α : Type u} {R : Type u_2} [TopologicalSpace α] [PseudoMetricSpace R] [AddZeroClass R] [BoundedAdd R] [ContinuousAdd R] : AddZeroClass (BoundedContinuousFunction α R)

def MonoidHom.compLeftContinuousBounded {β : Type v} {γ : Type w} (α : Type u_3) [TopologicalSpace α] [PseudoMetricSpace β] [Monoid β] [BoundedMul β] [ContinuousMul β] [PseudoMetricSpace γ] [Monoid γ] [BoundedMul γ] [ContinuousMul γ] (g : β →* γ) {C : NNReal} (hg : LipschitzWith C ⇑g) : BoundedContinuousFunction α β →* BoundedContinuousFunction α γ

Composition on the left by a (lipschitz-continuous) homomorphism of topological monoids, as a MonoidHom. Similar to MonoidHom.compLeftContinuous.

def AddMonoidHom.compLeftContinuousBounded {β : Type v} {γ : Type w} (α : Type u_3) [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] [PseudoMetricSpace γ] [AddMonoid γ] [BoundedAdd γ] [ContinuousAdd γ] (g : β →+ γ) {C : NNReal} (hg : LipschitzWith C ⇑g) : BoundedContinuousFunction α β →+ BoundedContinuousFunction α γ

Composition on the left by a (lipschitz-continuous) homomorphism of topological AddMonoids, as a AddMonoidHom. Similar to AddMonoidHom.compLeftContinuous.

@[simp]

theorem AddMonoidHom.compLeftContinuousBounded_apply {β : Type v} {γ : Type w} (α : Type u_3) [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] [PseudoMetricSpace γ] [AddMonoid γ] [BoundedAdd γ] [ContinuousAdd γ] (g : β →+ γ) {C : NNReal} (hg : LipschitzWith C ⇑g) (f : BoundedContinuousFunction α β) : (AddMonoidHom.compLeftContinuousBounded α g hg) f = BoundedContinuousFunction.comp (⇑g) hg f

@[simp]

theorem MonoidHom.compLeftContinuousBounded_apply {β : Type v} {γ : Type w} (α : Type u_3) [TopologicalSpace α] [PseudoMetricSpace β] [Monoid β] [BoundedMul β] [ContinuousMul β] [PseudoMetricSpace γ] [Monoid γ] [BoundedMul γ] [ContinuousMul γ] (g : β →* γ) {C : NNReal} (hg : LipschitzWith C ⇑g) (f : BoundedContinuousFunction α β) : (MonoidHom.compLeftContinuousBounded α g hg) f = BoundedContinuousFunction.comp (⇑g) hg f

@[simp]

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

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

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

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

@[simp]

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

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.

@[simp]

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

@[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 α β)

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.

theorem BoundedContinuousFunction.sub_apply {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Sub R] [BoundedSub R] [ContinuousSub R] (f 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 g : BoundedContinuousFunction α R) : ⇑(f - g) = ⇑f - ⇑g

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

@[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 α β)

@[simp]

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

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

IsBoundedSMul (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 IsBoundedSMul 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 𝕜 β] [IsBoundedSMul 𝕜 β] : SMul 𝕜 (BoundedContinuousFunction α β)

@[simp]

theorem BoundedContinuousFunction.coe_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [IsBoundedSMul 𝕜 β] (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 𝕜 β] [IsBoundedSMul 𝕜 β] (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 𝕜 β] [IsBoundedSMul 𝕜 β] {𝕜' : Type u_3} [PseudoMetricSpace 𝕜'] [Zero 𝕜'] [SMul 𝕜' β] [IsBoundedSMul 𝕜' β] [SMul 𝕜' 𝕜] [IsScalarTower 𝕜' 𝕜 β] : IsScalarTower 𝕜' 𝕜 (BoundedContinuousFunction α β)

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

theorem BoundedContinuousFunction.NNReal.upper_bound {α : Type u_2} [TopologicalSpace α] (f : BoundedContinuousFunction α NNReal) (x : α) : f x ≤ nndist f 0