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.

Equations

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

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

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

Equations

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

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

@[instance_reducible]

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

Equations

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

@[simp]

theorem BoundedContinuousFunction.coe_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.

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

@[simp]

theorem BoundedContinuousFunction.coe_mk {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : α → β) (h : Continuous f) (h' : ∃ (C : ℝ), ∀ (x y : α), dist ({ toFun := f, continuous_toFun := h }.toFun x) ({ toFun := f, continuous_toFun := h }.toFun y) ≤ C) : ⇑{ toFun := f, continuous_toFun := h, map_bounded' := h' } = f

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.

Equations

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

@[simp]

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

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

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

Equations

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

@[simp]

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

Equations

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

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

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

The uniform distance between two bounded continuous functions.

Equations

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

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

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

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

Equations

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

@[instance_reducible]

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

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

Equations

• BoundedContinuousFunction.instMetricSpace = { toPseudoMetricSpace := BoundedContinuousFunction.instPseudoMetricSpace, eq_of_dist_eq_zero := ⋯ }

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.

Equations

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

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

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

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

Equations

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

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

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

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

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

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

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.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

Restrict the domain of a bounded continuous function to a set.

Equations

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

@[simp]

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

@[simp]

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

@[deprecated BoundedContinuousFunction.domRestrict (since := "2026-07-19")]

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

Alias of BoundedContinuousFunction.domRestrict.

---

Restrict the domain of a bounded continuous function to a set.

Equations

• @BoundedContinuousFunction.restrict = @BoundedContinuousFunction.domRestrict

@[deprecated BoundedContinuousFunction.coe_domRestrict (since := "2026-07-19")]

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

Alias of BoundedContinuousFunction.coe_domRestrict.

@[deprecated BoundedContinuousFunction.domRestrict_apply (since := "2026-07-19")]

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

Alias of BoundedContinuousFunction.domRestrict_apply.

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

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

Equations

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

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

Equations

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

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

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

Equations

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

@[simp]

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

Equations

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

@[simp]

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

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

@[deprecated FunLike.coe_zero (since := "2026-10-20")]

theorem BoundedContinuousFunction.coe_zero {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [Zero F] [Zero β] [IsZeroApply F] : ⇑0 = 0

Alias of FunLike.coe_zero.

@[deprecated FunLike.coe_one (since := "2026-10-20")]

theorem BoundedContinuousFunction.coe_one {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [One F] [One β] [IsOneApply F] : ⇑1 = 1

Alias of FunLike.coe_one.

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

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

Equations

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

@[instance_reducible]

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

Equations

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

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

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

@[deprecated FunLike.coe_add (since := "2026-10-20")]

theorem BoundedContinuousFunction.coe_add {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [Add F] [Add β] [IsAddApply F] (f g : F) : ⇑(f + g) = ⇑f + ⇑g

Alias of FunLike.coe_add.

@[deprecated FunLike.coe_mul (since := "2026-10-20")]

theorem BoundedContinuousFunction.coe_mul {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [Mul F] [Mul β] [IsMulApply F] (f g : F) : ⇑(f * g) = ⇑f * ⇑g

Alias of FunLike.coe_mul.

@[deprecated add_apply (since := "2026-10-20")]

theorem BoundedContinuousFunction.add_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Add β} {inst✝² : Add F} [self : IsAddApply F] (f g : F) (x : α) : (f + g) x = f x + g x

Alias of add_apply.

@[deprecated mul_apply (since := "2026-10-20")]

theorem BoundedContinuousFunction.mul_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Mul β} {inst✝² : Mul F} [self : IsMulApply F] (f g : F) (x : α) : (f * g) x = f x * g x

Alias of mul_apply.

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

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

@[deprecated FunLike.coe_smul (since := "2026-10-20")]

theorem BoundedContinuousFunction.coe_nsmul {M : Type u_1} {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [SMul M F] [SMul M β] [IsSMulApply M F] (n : M) (f : F) : ⇑(n • f) = n • ⇑f

Alias of FunLike.coe_smul.

@[deprecated FunLike.coe_pow (since := "2026-10-20")]

theorem BoundedContinuousFunction.coe_pow {M : Type u_1} {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [Pow F M] [Pow β M] [IsPowApply M F] (f : F) (n : M) : ⇑(f ^ n) = ⇑f ^ n

Alias of FunLike.coe_pow.

@[deprecated smul_apply (since := "2026-10-20")]

theorem BoundedContinuousFunction.nsmul_apply {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst✝ : FunLike F α β} {inst✝¹ : SMul M β} {inst✝² : SMul M F} [self : IsSMulApply M F] (f : F) (n : M) (x : α) : (n • f) x = n • f x

Alias of smul_apply.

@[deprecated pow_apply (since := "2026-10-20")]

theorem BoundedContinuousFunction.pow_apply {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst✝ : FunLike F α β} {inst✝¹ : Pow β M} {inst✝² : Pow F M} [self : IsPowApply M F] (f : F) (n : M) (x : α) : (f ^ n) x = f x ^ n

Alias of pow_apply.

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• BoundedContinuousFunction.instCommMonoid = { toMonoid := BoundedContinuousFunction.instMonoid, mul_comm := ⋯ }

@[instance_reducible]

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

Equations

• BoundedContinuousFunction.instAddCommMonoid = { toAddMonoid := BoundedContinuousFunction.instAddMonoid, add_comm := ⋯ }

@[deprecated FunLike.coeAddMonoidHom (since := "2026-10-20")]

def BoundedContinuousFunction.coeFnAddMonoidHom (F : Type u_1) (α : Type u_2) (β : Type u_3) [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F] [IsAddApply F] : F →+ α → β

Alias of FunLike.coeAddMonoidHom.

Equations

• BoundedContinuousFunction.coeFnAddMonoidHom = FunLike.coeAddMonoidHom

@[deprecated FunLike.coeMonoidHom (since := "2026-10-20")]

def BoundedContinuousFunction.coeFnMonoidHom (F : Type u_1) (α : Type u_2) (β : Type u_3) [FunLike F α β] [MulOne F] [MulOneClass β] [IsOneApply F] [IsMulApply F] : F →* α → β

Alias of FunLike.coeMonoidHom.

Equations

• BoundedContinuousFunction.coeFnMonoidHom = FunLike.coeMonoidHom

def BoundedContinuousFunction.toContinuousMapMonoidHom (α : Type u) (R : Type u_2) [TopologicalSpace α] [PseudoMetricSpace R] [Monoid R] [BoundedMul R] [ContinuousMul R] : BoundedContinuousFunction α R →* C(α, R)

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

Equations

• BoundedContinuousFunction.toContinuousMapMonoidHom α R = { toFun := BoundedContinuousFunction.toContinuousMap, map_one' := ⋯, map_mul' := ⋯ }

def BoundedContinuousFunction.toContinuousMapAddMonoidHom (α : Type u) (R : Type u_2) [TopologicalSpace α] [PseudoMetricSpace R] [AddMonoid R] [BoundedAdd R] [ContinuousAdd R] : BoundedContinuousFunction α R →+ C(α, R)

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

Equations

• BoundedContinuousFunction.toContinuousMapAddMonoidHom α R = { toFun := BoundedContinuousFunction.toContinuousMap, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.toContinuousMapAddMonoidHom_apply (α : Type u) (R : Type u_2) [TopologicalSpace α] [PseudoMetricSpace R] [AddMonoid R] [BoundedAdd R] [ContinuousAdd R] (self : BoundedContinuousFunction α R) : (toContinuousMapAddMonoidHom α R) self = self.toContinuousMap

@[simp]

theorem BoundedContinuousFunction.toContinuousMapMonoidHom_apply (α : Type u) (R : Type u_2) [TopologicalSpace α] [PseudoMetricSpace R] [Monoid R] [BoundedMul R] [ContinuousMul R] (self : BoundedContinuousFunction α R) : (toContinuousMapMonoidHom α R) self = self.toContinuousMap

@[deprecated FunLike.coe_sum (since := "2026-10-20")]

theorem BoundedContinuousFunction.coe_sum {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [FunLike F α β] [AddCommMonoid β] [AddCommMonoid F] [IsZeroApply F] [IsAddApply F] (s : Finset ι) (f : ι → F) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

Alias of FunLike.coe_sum.

@[deprecated FunLike.coe_prod (since := "2026-10-20")]

theorem BoundedContinuousFunction.coe_prod {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [FunLike F α β] [CommMonoid β] [CommMonoid F] [IsOneApply F] [IsMulApply F] (s : Finset ι) (f : ι → F) : ⇑(∏ i ∈ s, f i) = ∏ i ∈ s, ⇑(f i)

Alias of FunLike.coe_prod.

@[deprecated sum_apply (since := "2026-10-20")]

theorem BoundedContinuousFunction.sum_apply {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [FunLike F α β] [AddCommMonoid β] [AddCommMonoid F] [IsZeroApply F] [IsAddApply F] (s : Finset ι) (f : ι → F) (x : α) : (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x

Alias of sum_apply.

@[deprecated prod_apply (since := "2026-10-20")]

theorem BoundedContinuousFunction.prod_apply {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [FunLike F α β] [CommMonoid β] [CommMonoid F] [IsOneApply F] [IsMulApply F] (s : Finset ι) (f : ι → F) (x : α) : (∏ i ∈ s, f i) x = ∏ i ∈ s, (f i) x

Alias of prod_apply.

@[instance_reducible]

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

Equations

• BoundedContinuousFunction.instMulOneClass = { toOne := BoundedContinuousFunction.instOne, toMul := BoundedContinuousFunction.instMul, one_mul := ⋯, mul_one := ⋯ }

@[instance_reducible]

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

Equations

• BoundedContinuousFunction.instAddZeroClass = { toZero := BoundedContinuousFunction.instZero, toAdd := BoundedContinuousFunction.instAdd, zero_add := ⋯, add_zero := ⋯ }

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.

Equations

• MonoidHom.compLeftContinuousBounded α g hg = { toFun := fun (f : BoundedContinuousFunction α β) => BoundedContinuousFunction.comp (⇑g) hg f, map_one' := ⋯, map_mul' := ⋯ }

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.

Equations

• AddMonoidHom.compLeftContinuousBounded α g hg = { toFun := fun (f : BoundedContinuousFunction α β) => BoundedContinuousFunction.comp (⇑g) hg f, map_zero' := ⋯, map_add' := ⋯ }

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

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

@[instance_reducible]

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

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

Equations

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

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

@[deprecated FunLike.coe_sub (since := "2026-10-20")]

theorem BoundedContinuousFunction.coe_sub {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [Sub F] [Sub β] [IsSubApply F] (f g : F) : ⇑(f - g) = ⇑f - ⇑g

Alias of FunLike.coe_sub.

@[deprecated sub_apply (since := "2026-10-20")]

theorem BoundedContinuousFunction.sub_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Sub β} {inst✝² : Sub F} [self : IsSubApply F] (f g : F) (x : α) : (f - g) x = f x - g x

Alias of sub_apply.

@[instance_reducible]

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

Equations

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

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

@[deprecated natCast_apply_eq_const (since := "2026-10-20")]

theorem BoundedContinuousFunction.natCast_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : NatCast F} {inst✝² : NatCast β} [self : IsNatCastApply F] (n : ℕ) (x : α) : ↑n x = ↑n

Alias of natCast_apply_eq_const.

@[instance_reducible]

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

Equations

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

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

@[deprecated intCast_apply_eq_const (since := "2026-10-20")]

theorem BoundedContinuousFunction.intCast_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : IntCast F} {inst✝² : IntCast β} [self : IsIntCastApply F] (n : ℤ) (x : α) : ↑n x = ↑n

Alias of intCast_apply_eq_const.

@[instance_reducible]

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)

Equations

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

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_reducible]

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

Equations

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

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

@[deprecated FunLike.coe_smul (since := "2026-10-20")]

theorem BoundedContinuousFunction.coe_smul {M : Type u_1} {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [SMul M F] [SMul M β] [IsSMulApply M F] (n : M) (f : F) : ⇑(n • f) = n • ⇑f

Alias of FunLike.coe_smul.

@[deprecated smul_apply (since := "2026-10-20")]

theorem BoundedContinuousFunction.smul_apply {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst✝ : FunLike F α β} {inst✝¹ : SMul M β} {inst✝² : SMul M F} [self : IsSMulApply M F] (f : F) (n : M) (x : α) : (n • f) x = n • f x

Alias of smul_apply.

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_reducible]

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

Equations

• BoundedContinuousFunction.instMulAction = { toSMul := BoundedContinuousFunction.instSMul, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

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

Equations

• BoundedContinuousFunction.instDistribMulAction = { toMulAction := BoundedContinuousFunction.instMulAction, smul_zero := ⋯, smul_add := ⋯ }

@[instance_reducible]

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

Equations

• BoundedContinuousFunction.instModule = { toDistribMulAction := BoundedContinuousFunction.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

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

Equations

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

@[simp]

theorem BoundedContinuousFunction.evalCLM_apply {α : Type u} {β : Type v} (𝕜 : Type u_2) [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Semiring 𝕜] [AddCommMonoid β] [Module 𝕜 β] [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.

Equations

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

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