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

Instances For

source

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.

source

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

Instances

source

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

FunLike (BoundedContinuousFunction α β) α β

Equations

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

source

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

BoundedContinuousMapClass (BoundedContinuousFunction α β) α β

source

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' := ⋯ } }

source

@[simp]

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

⇑f.toContinuousMap = ⇑f

source

@[deprecated BoundedContinuousFunction.coe_toContinuousMap (since := "2024-11-23")]

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

⇑f.toContinuousMap = ⇑f

Alias of BoundedContinuousFunction.coe_toContinuousMap.

source

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

source

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

∃ (C : ℝ), ∀ (x y : α), dist (f x) (f y) ≤ C

source

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

Continuous ⇑f

source

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

f = g

source

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

Bornology.IsBounded (Set.range ⇑f)

source

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

Bornology.IsBounded (⇑f '' s)

source

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

f = g

source

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' := ⋯ }

source

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

source

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' := ⋯ }

source

@[simp]

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

(mkOfCompact f) a = f a

source

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' := ⋯ }

source

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

source

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

source

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}

source

theorem BoundedContinuousFunction.dist_set_exists {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f g : BoundedContinuousFunction α β} :

∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C

source

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.

source

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.

source

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

source

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

source

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

source

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

source

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.

source

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

MetricSpace (BoundedContinuousFunction α β)

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

Equations

BoundedContinuousFunction.instMetricSpace = MetricSpace.mk ⋯

source

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}

source

theorem BoundedContinuousFunction.nndist_set_exists {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f g : BoundedContinuousFunction α β} :

∃ (C : NNReal), ∀ (x : α), nndist (f x) (g x) ≤ C

source

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

nndist (f x) (g x) ≤ nndist f g

source

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.

source

theorem BoundedContinuousFunction.dist_eq_iSup {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f g : BoundedContinuousFunction α β} :

dist f g = ⨆ (x : α), dist (f x) (g x)

source

theorem BoundedContinuousFunction.nndist_eq_iSup {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f g : BoundedContinuousFunction α β} :

nndist f g = ⨆ (x : α), nndist (f x) (g x)

source

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

source

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

source

@[deprecated BoundedContinuousFunction.isInducing_coeFn (since := "2024-10-28")]

theorem BoundedContinuousFunction.inducing_coeFn {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] :

Topology.IsInducing (⇑UniformFun.ofFun ∘ DFunLike.coe)

Alias of BoundedContinuousFunction.isInducing_coeFn.

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

source

theorem BoundedContinuousFunction.isEmbedding_coeFn {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] :

Topology.IsEmbedding (⇑UniformFun.ofFun ∘ DFunLike.coe)

source

@[deprecated BoundedContinuousFunction.isEmbedding_coeFn (since := "2024-10-26")]

theorem BoundedContinuousFunction.embedding_coeFn {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] :

Topology.IsEmbedding (⇑UniformFun.ofFun ∘ DFunLike.coe)

Alias of BoundedContinuousFunction.isEmbedding_coeFn.

source

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' := ⋯ }

source

@[simp]

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

⇑(const α b) = fun (x : α) => b

source

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

(const α b) a = b

source

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 }

source

theorem BoundedContinuousFunction.lipschitz_evalx {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (x : α) :

LipschitzWith 1 fun (f : BoundedContinuousFunction α β) => f x

source

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

UniformContinuous DFunLike.coe

source

theorem BoundedContinuousFunction.continuous_coe {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] :

Continuous fun (f : BoundedContinuousFunction α β) (x : α) => f x

source

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.

source

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.

source

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.

source

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' := ⋯ }

source

@[simp]

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

⇑(f.compContinuous g) = ⇑f ∘ ⇑g

source

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

source

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

LipschitzWith 1 fun (f : BoundedContinuousFunction α β) => f.compContinuous g

source

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

Continuous fun (f : BoundedContinuousFunction α β) => f.compContinuous g

source

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

BoundedContinuousFunction (↑s) β

Restrict a bounded continuous function to a set.

Equations

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

source

@[simp]

theorem BoundedContinuousFunction.coe_restrict {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) (s : Set α) :

⇑(f.restrict s) = ⇑f ∘ Subtype.val

source

@[simp]

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

(f.restrict s) x = f ↑x

source

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' := ⋯ }

source

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.

source

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.

source

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.

source

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' := ⋯ }

source

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' := ⋯ }

source

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

source

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

source

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

source

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

source

@[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₂) = dist g₁ g₂ ⊔ dist (h₁.restrict (Set.range ⇑f)ᶜ) (h₂.restrict (Set.range ⇑f)ᶜ)

source

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

source

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' := ⋯ }

source

@[simp]

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

(indicator s hs) x = s.indicator 1 x

source

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

IsCompact A

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

source

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

IsCompact A

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

source

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

IsCompact (closure A)

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

source

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

One (BoundedContinuousFunction α β)

Equations

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

source

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

Zero (BoundedContinuousFunction α β)

Equations

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

source

@[simp]

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

⇑1 = 1

source

@[simp]

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

⇑0 = 0

source

@[simp]

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

mkOfCompact 1 = 1

source

@[simp]

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

mkOfCompact 0 = 0

source

theorem BoundedContinuousFunction.forall_coe_one_iff_one {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [One β] (f : BoundedContinuousFunction α β) :

(∀ (x : α), f x = 1) ↔ f = 1

source

theorem BoundedContinuousFunction.forall_coe_zero_iff_zero {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] (f : BoundedContinuousFunction α β) :

(∀ (x : α), f x = 0) ↔ f = 0

source

@[simp]

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

compContinuous 1 f = 1

source

@[simp]

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

compContinuous 0 f = 0

source

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

Add (BoundedContinuousFunction α β)

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

Equations

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

source

@[simp]

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

⇑(f + g) = ⇑f + ⇑g

source

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

(f + g) x = f x + g x

source

@[simp]

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

mkOfCompact (f + g) = mkOfCompact f + mkOfCompact g

source

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

(g + f).compContinuous h = g.compContinuous h + f.compContinuous h

source

@[simp]

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

⇑(nsmulRec n f) = n • ⇑f

source

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

SMul ℕ (BoundedContinuousFunction α β)

Equations

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

source

@[simp]

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

⇑(r • f) = r • ⇑f

source

@[simp]

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

(r • f) v = r • f v

source

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

AddMonoid (BoundedContinuousFunction α β)

Equations

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

source

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

BoundedContinuousFunction α β →+ α → β

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

Equations

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

source

@[simp]

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

coeFnAddHom a✝ a = a✝ a

source

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

BoundedContinuousFunction α β →+ C(α, β)

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

Equations

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

source

@[simp]

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

(toContinuousMapAddHom α β) self = self.toContinuousMap

source

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

AddCommMonoid (BoundedContinuousFunction α β)

Equations

BoundedContinuousFunction.instAddCommMonoid = AddCommMonoid.mk ⋯

source

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

AddCommMonoid (BoundedContinuousFunction α β)

Equations

BoundedContinuousFunction.instAddAddCommMonoid = AddCommMonoid.mk ⋯

source

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

source

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

source

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

LipschitzAdd (BoundedContinuousFunction α β)

source

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' := ⋯ } }

source

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

source

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

source

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

NatCast (BoundedContinuousFunction α β)

Equations

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

source

@[simp]

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

↑n x = ↑n

source

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

IntCast (BoundedContinuousFunction α β)

Equations

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

source

@[simp]

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

↑m x = ↑m

source

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

Mul (BoundedContinuousFunction α R)

Equations

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

source

@[simp]

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

⇑(f * g) = ⇑f * ⇑g

source

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

(f * g) x = f x * g x

source

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

Pow (BoundedContinuousFunction α R) ℕ

Equations

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

source

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

⇑(f ^ n) = ⇑f ^ n

source

@[simp]

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

(f ^ n) x = f x ^ n

source

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

Monoid (BoundedContinuousFunction α R)

Equations

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

source

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

CommMonoid (BoundedContinuousFunction α R)

Equations

BoundedContinuousFunction.instCommMonoid = CommMonoid.mk ⋯

source

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

Semiring (BoundedContinuousFunction α R)

Equations

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

source

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

Norm (BoundedContinuousFunction α β)

Equations

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

source

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

‖f‖ = dist f 0

source

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.

source

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.

source

@[simp]

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

‖f‖ = 0

source

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

‖f x‖ ≤ ‖f‖

source

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

-‖f‖ ≤ f x

source

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

f x ≤ ‖f‖

source

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

source

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.

source

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.

source

theorem BoundedContinuousFunction.norm_le_of_nonempty {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [Nonempty α] {f : BoundedContinuousFunction α β} {M : ℝ} :

‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M

source

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

source

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

source

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

‖const α b‖ ≤ ‖b‖

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

source

@[simp]

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

‖const α b‖ = ‖b‖

source

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

BoundedContinuousFunction α β

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

Equations

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

source

@[simp]

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

⇑(ofNormedAddCommGroup f Hf C H) = f

source

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

‖ofNormedAddCommGroup f hfc C hfC‖ ≤ C

source

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

BoundedContinuousFunction α β

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

Equations

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

source

@[simp]

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

⇑(ofNormedAddCommGroupDiscrete f C H) = f

source

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

BoundedContinuousFunction α ℝ

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

Equations

f.normComp = BoundedContinuousFunction.comp norm ⋯ f

source

@[simp]

theorem BoundedContinuousFunction.coe_normComp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) :

⇑f.normComp = norm ∘ ⇑f

source

@[simp]

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

‖f.normComp‖ = ‖f‖

source

theorem BoundedContinuousFunction.bddAbove_range_norm_comp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) :

BddAbove (Set.range (norm ∘ ⇑f))

source

theorem BoundedContinuousFunction.norm_eq_iSup_norm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) :

‖f‖ = ⨆ (x : α), ‖f x‖

source

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

NormOneClass (BoundedContinuousFunction α β)

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

source

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

Neg (BoundedContinuousFunction α β)

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

Equations

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

source

@[simp]

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

⇑(-f) = -⇑f

source

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

(-f) x = -f x

source

@[simp]

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

mkOfCompact (-f) = -mkOfCompact f

source

@[simp]

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

mkOfCompact (f - g) = mkOfCompact f - mkOfCompact g

source

@[simp]

theorem BoundedContinuousFunction.coe_zsmulRec {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (z : ℤ) :

⇑(zsmulRec (fun (x1 : ℕ) (x2 : BoundedContinuousFunction α β) => x1 • x2) z f) = z • ⇑f

source

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

SMul ℤ (BoundedContinuousFunction α β)

Equations

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

source

@[simp]

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

⇑(r • f) = r • ⇑f

source

@[simp]

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

(r • f) v = r • f v

source

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

AddCommGroup (BoundedContinuousFunction α β)

Equations

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

source

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

SeminormedAddCommGroup (BoundedContinuousFunction α β)

Equations

BoundedContinuousFunction.instSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯

source

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

NormedAddCommGroup (BoundedContinuousFunction α β)

Equations

BoundedContinuousFunction.instNormedAddCommGroup = NormedAddCommGroup.mk ⋯

source

theorem BoundedContinuousFunction.nnnorm_def {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) :

‖f‖₊ = nndist f 0

source

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

‖f x‖₊ ≤ ‖f‖₊

source

theorem BoundedContinuousFunction.nndist_le_two_nnnorm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (x y : α) :

nndist (f x) (f y) ≤ 2 * ‖f‖₊

source

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.

source

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

‖const α b‖₊ ≤ ‖b‖₊

source

@[simp]

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

‖const α b‖₊ = ‖b‖₊

source

theorem BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) :

‖f‖₊ = ⨆ (x : α), ‖f x‖₊

source

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

‖f x - g x‖ ≤ dist f g

source

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

f x ≤ g x + dist f g

source

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

‖f.compContinuous g‖ ≤ ‖f‖

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

source

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

SMul 𝕜 (BoundedContinuousFunction α β)

Equations

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

source

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

source

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

source

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

source

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

source

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

IsCentralScalar 𝕜 (BoundedContinuousFunction α β)

source

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

IsBoundedSMul 𝕜 (BoundedContinuousFunction α β)

source

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

MulAction 𝕜 (BoundedContinuousFunction α β)

Equations

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

source

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

DistribMulAction 𝕜 (BoundedContinuousFunction α β)

Equations

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

source

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

Module 𝕜 (BoundedContinuousFunction α β)

Equations

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

source

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 := ⋯ }

source

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

source

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' := ⋯ }

source

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

Normed space structure #

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

source

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

NormedSpace 𝕜 (BoundedContinuousFunction α β)

Equations

BoundedContinuousFunction.instNormedSpace = NormedSpace.mk ⋯

source

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.

source

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

source

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

NonUnitalRing (BoundedContinuousFunction α R)

Equations

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

source

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

NonUnitalSeminormedRing (BoundedContinuousFunction α R)

Equations

BoundedContinuousFunction.instNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

source

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

NonUnitalSeminormedCommRing (BoundedContinuousFunction α R)

Equations

BoundedContinuousFunction.instNonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

source

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

NonUnitalNormedRing (BoundedContinuousFunction α R)

Equations

BoundedContinuousFunction.instNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

source

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

NonUnitalNormedCommRing (BoundedContinuousFunction α R)

Equations

BoundedContinuousFunction.instNonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

source

@[simp]

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

⇑(npowRec n f) = ⇑f ^ n

source

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

Pow (BoundedContinuousFunction α R) ℕ

Equations

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

source

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

NatCast (BoundedContinuousFunction α R)

Equations

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

source

@[simp]

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

⇑↑n = ↑n

source

@[simp]

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

⇑(OfNat.ofNat n) = OfNat.ofNat n

source

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

IntCast (BoundedContinuousFunction α R)

Equations

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

source

@[simp]

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

⇑↑n = ↑n

source

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

Ring (BoundedContinuousFunction α R)

Equations

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

source

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

SeminormedRing (BoundedContinuousFunction α R)

Equations

BoundedContinuousFunction.instSeminormedRing = SeminormedRing.mk ⋯ ⋯

source

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

NormedRing (BoundedContinuousFunction α R)

Equations

BoundedContinuousFunction.instNormedRing = NormedRing.mk ⋯ ⋯

Normed commutative ring structure #

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

source

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

CommRing (BoundedContinuousFunction α R)

Equations

BoundedContinuousFunction.instCommRing = CommRing.mk ⋯

source

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

SeminormedCommRing (BoundedContinuousFunction α R)

Equations

BoundedContinuousFunction.instSeminormedCommRing = SeminormedCommRing.mk ⋯

source

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

NormedCommRing (BoundedContinuousFunction α R)

Equations

BoundedContinuousFunction.instNormedCommRing = NormedCommRing.mk ⋯

source

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

IsScalarTower 𝕜 (BoundedContinuousFunction α β) (BoundedContinuousFunction α β)

source

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

SMulCommClass 𝕜 (BoundedContinuousFunction α β) (BoundedContinuousFunction α β)

source

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

SMulCommClass (BoundedContinuousFunction α β) 𝕜 (BoundedContinuousFunction α β)

Normed algebra structure #

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

source

def BoundedContinuousFunction.C {α : Type u} {γ : Type w} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] :

𝕜 →+* BoundedContinuousFunction α γ

BoundedContinuousFunction.const as a RingHom.

Equations

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

source

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

Algebra 𝕜 (BoundedContinuousFunction α γ)

Equations

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

source

@[simp]

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

((algebraMap 𝕜 (BoundedContinuousFunction α γ)) k) a = k • 1

source

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

NormedAlgebra 𝕜 (BoundedContinuousFunction α γ)

Equations

BoundedContinuousFunction.instNormedAlgebra = NormedAlgebra.mk ⋯

Structure as normed module over scalar functions #

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

source

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

SMul (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)

Equations

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

source

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

Module (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)

Equations

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

source

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

IsBoundedSMul (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)

source

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

f x ≤ nndist f 0

source

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

PartialOrder (BoundedContinuousFunction α β)

Equations

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

source

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

Max (BoundedContinuousFunction α β)

Equations

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

source

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

Min (BoundedContinuousFunction α β)

Equations

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