Documentation

Mathlib.Topology.ContinuousFunction.Bounded

Bounded continuous functions #

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

structure BoundedContinuousFunction (α : Type u) (β : Type v) [TopologicalSpace α] [PseudoMetricSpace β] extends ContinuousMap :
Type (max u v)

α →ᵇ β is the type of bounded continuous functions α → β from a topological space to a metric space.

When possible, instead of parametrizing results over (f : α →ᵇ β), you should parametrize over (F : Type*) [BoundedContinuousMapClass F α β] (f : F).

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

  • toFun : αβ
  • continuous_toFun : Continuous self.toFun
  • map_bounded' : ∃ (C : ), ∀ (x y : α), dist (self.toFun x) (self.toFun y) C
Instances For
    theorem BoundedContinuousFunction.map_bounded' {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (self : BoundedContinuousFunction α β) :
    ∃ (C : ), ∀ (x y : α), dist (self.toFun x) (self.toFun y) C
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      class BoundedContinuousMapClass (F : Type u_2) (α : outParam (Type u_3)) (β : outParam (Type u_4)) [TopologicalSpace α] [PseudoMetricSpace β] [FunLike F α β] extends ContinuousMapClass :

      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
        theorem BoundedContinuousMapClass.map_bounded {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} [TopologicalSpace α] [PseudoMetricSpace β] [FunLike F α β] [self : BoundedContinuousMapClass F α β] (f : F) :
        ∃ (C : ), ∀ (x y : α), dist (f x) (f y) C
        Equations
        Equations
        • BoundedContinuousFunction.instCoeTC = { coe := fun (f : F) => { toFun := f, continuous_toFun := , map_bounded' := } }
        @[simp]
        theorem BoundedContinuousFunction.coe_to_continuous_fun {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) :
        f.toContinuousMap = f

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

        Equations
        Instances For
          theorem BoundedContinuousFunction.bounded {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) :
          ∃ (C : ), ∀ (x y : α), dist (f x) (f y) C
          theorem BoundedContinuousFunction.ext {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} (h : ∀ (x : α), f x = g x) :
          f = g
          def BoundedContinuousFunction.mkOfBound {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : C(α, β)) (C : ) (h : ∀ (x y : α), dist (f x) (f y) C) :

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

          Equations
          Instances For
            @[simp]
            theorem BoundedContinuousFunction.mkOfBound_coe {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : C(α, β)} {C : } {h : ∀ (x y : α), dist (f x) (f y) C} :

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

            Equations
            Instances For
              @[simp]
              theorem BoundedContinuousFunction.mkOfDiscrete_toFun {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [DiscreteTopology α] (f : αβ) (C : ) (h : ∀ (x y : α), dist (f x) (f y) C) :
              ∀ (a : α), (BoundedContinuousFunction.mkOfDiscrete f C h) a = f a
              @[simp]
              theorem BoundedContinuousFunction.mkOfDiscrete_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [DiscreteTopology α] (f : αβ) (C : ) (h : ∀ (x y : α), dist (f x) (f y) C) :
              ∀ (a : α), (BoundedContinuousFunction.mkOfDiscrete f C h) a = f a
              def BoundedContinuousFunction.mkOfDiscrete {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [DiscreteTopology α] (f : αβ) (C : ) (h : ∀ (x y : α), dist (f x) (f y) C) :

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

                The uniform distance between two bounded continuous functions.

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

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

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

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

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

                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.

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

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

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

                theorem BoundedContinuousFunction.dist_eq_iSup {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} :
                dist f g = ⨆ (x : α), dist (f x) (g x)
                theorem BoundedContinuousFunction.nndist_eq_iSup {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f : BoundedContinuousFunction α β} {g : BoundedContinuousFunction α β} :
                nndist f g = ⨆ (x : α), nndist (f x) (g x)
                theorem BoundedContinuousFunction.tendsto_iff_tendstoUniformly {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {ι : Type u_2} {F : ιBoundedContinuousFunction α β} {f : BoundedContinuousFunction α β} {l : Filter ι} :
                Filter.Tendsto F l (nhds f) TendstoUniformly (fun (i : ι) => (F i)) (f) l
                theorem BoundedContinuousFunction.inducing_coeFn {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] :
                Inducing (UniformFun.ofFun DFunLike.coe)

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

                theorem BoundedContinuousFunction.embedding_coeFn {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] :
                Embedding (UniformFun.ofFun DFunLike.coe)
                @[simp]
                theorem BoundedContinuousFunction.const_apply (α : Type u) {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (b : β) :
                (BoundedContinuousFunction.const α b) = fun (x : α) => b
                @[simp]
                theorem BoundedContinuousFunction.const_toFun (α : Type u) {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (b : β) :
                (BoundedContinuousFunction.const α b) = fun (x : α) => b

                Constant as a continuous bounded function.

                Equations
                Instances For

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

                  Equations

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

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

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

                  Equations
                  • =

                  Composition of a bounded continuous function and a continuous function.

                  Equations
                  • f.compContinuous g = { toContinuousMap := f.comp g, map_bounded' := }
                  Instances For
                    @[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

                    Restrict a bounded continuous function to a set.

                    Equations
                    Instances For
                      @[simp]
                      theorem BoundedContinuousFunction.coe_restrict {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) (s : Set α) :
                      (f.restrict s) = f Subtype.val
                      @[simp]
                      theorem BoundedContinuousFunction.restrict_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] (f : BoundedContinuousFunction α β) (s : Set α) (x : s) :
                      (f.restrict s) x = f x

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

                      Equations
                      Instances For

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

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

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

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

                        Equations
                        Instances For

                          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
                          Instances For
                            @[simp]
                            theorem BoundedContinuousFunction.extend_apply' {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] [DiscreteTopology δ] {f : α δ} {x : δ} (hx : xSet.range f) (g : BoundedContinuousFunction α β) (h : BoundedContinuousFunction δ β) :
                            @[simp]
                            theorem BoundedContinuousFunction.dist_extend_extend {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {δ : Type u_2} [TopologicalSpace δ] [DiscreteTopology δ] (f : α δ) (g₁ : BoundedContinuousFunction α β) (g₂ : BoundedContinuousFunction α β) (h₁ : BoundedContinuousFunction δ β) (h₂ : BoundedContinuousFunction δ β) :
                            dist (BoundedContinuousFunction.extend f g₁ h₁) (BoundedContinuousFunction.extend f g₂ h₂) = max (dist g₁ g₂) (dist (h₁.restrict (Set.range f)) (h₂.restrict (Set.range f)))
                            theorem BoundedContinuousFunction.arzela_ascoli₁ {α : Type u} {β : Type v} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] [CompactSpace β] (A : Set (BoundedContinuousFunction α β)) (closed : IsClosed A) (H : Equicontinuous fun (x : A) => x) :

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

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

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

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

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

                            Equations
                            Equations
                            @[simp]
                            theorem BoundedContinuousFunction.coe_zero {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] :
                            0 = 0
                            @[simp]
                            theorem BoundedContinuousFunction.coe_one {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [One β] :
                            1 = 1
                            theorem BoundedContinuousFunction.forall_coe_zero_iff_zero {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] (f : BoundedContinuousFunction α β) :
                            (∀ (x : α), f x = 0) f = 0
                            theorem BoundedContinuousFunction.forall_coe_one_iff_one {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [One β] (f : BoundedContinuousFunction α β) :
                            (∀ (x : α), f x = 1) f = 1

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

                            Equations
                            • BoundedContinuousFunction.instAdd = { add := fun (f g : BoundedContinuousFunction α β) => { toFun := fun (x : α) => f x + g x, continuous_toFun := , map_bounded' := } }
                            @[simp]
                            theorem BoundedContinuousFunction.coe_add {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) :
                            (f + g) = f + g
                            theorem BoundedContinuousFunction.add_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) {x : α} :
                            (f + g) x = f x + g x
                            theorem BoundedContinuousFunction.add_compContinuous {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (f : BoundedContinuousFunction α β) (g : BoundedContinuousFunction α β) [TopologicalSpace γ] (h : C(γ, α)) :
                            (g + f).compContinuous h = g.compContinuous h + f.compContinuous h
                            @[simp]
                            Equations
                            • BoundedContinuousFunction.instSMulNat = { smul := fun (n : ) (f : BoundedContinuousFunction α β) => { toContinuousMap := n f.toContinuousMap, map_bounded' := } }
                            @[simp]
                            theorem BoundedContinuousFunction.coe_nsmul {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (r : ) (f : BoundedContinuousFunction α β) :
                            (r f) = r f
                            @[simp]
                            theorem BoundedContinuousFunction.nsmul_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] (r : ) (f : BoundedContinuousFunction α β) (v : α) :
                            (r f) v = r f v
                            Equations
                            @[simp]
                            theorem BoundedContinuousFunction.coeFnAddHom_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] :
                            ∀ (a : BoundedContinuousFunction α β) (a_1 : α), BoundedContinuousFunction.coeFnAddHom a a_1 = a a_1

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

                            Equations
                            • BoundedContinuousFunction.coeFnAddHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
                            Instances For

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

                              Equations
                              Instances For
                                Equations
                                Equations
                                @[simp]
                                theorem BoundedContinuousFunction.coe_sum {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [BoundedAdd β] [ContinuousAdd β] {ι : Type u_2} (s : Finset ι) (f : ιBoundedContinuousFunction α β) :
                                (is, f i) = is, (f i)
                                theorem BoundedContinuousFunction.sum_apply {α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] [AddCommMonoid β] [BoundedAdd β] [ContinuousAdd β] {ι : Type u_2} (s : Finset ι) (f : ιBoundedContinuousFunction α β) (a : α) :
                                (is, f i) a = is, (f i) a

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

                                Equations
                                • BoundedContinuousFunction.instSub = { sub := fun (f g : BoundedContinuousFunction α R) => { toFun := fun (x : α) => f x - g x, continuous_toFun := , map_bounded' := } }
                                theorem BoundedContinuousFunction.sub_apply {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Sub R] [BoundedSub R] [ContinuousSub R] (f : BoundedContinuousFunction α R) (g : BoundedContinuousFunction α R) {x : α} :
                                (f - g) x = f x - g x
                                @[simp]
                                theorem BoundedContinuousFunction.coe_sub {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Sub R] [BoundedSub R] [ContinuousSub R] (f : BoundedContinuousFunction α R) (g : BoundedContinuousFunction α R) :
                                (f - g) = f - g
                                Equations
                                @[simp]
                                theorem BoundedContinuousFunction.natCast_apply {α : Type u} [TopologicalSpace α] {β : Type u_2} [PseudoMetricSpace β] [NatCast β] (n : ) (x : α) :
                                n x = n
                                Equations
                                @[simp]
                                theorem BoundedContinuousFunction.intCast_apply {α : Type u} [TopologicalSpace α] {β : Type u_2} [PseudoMetricSpace β] [IntCast β] (m : ) (x : α) :
                                m x = m
                                Equations
                                • BoundedContinuousFunction.instMul = { mul := fun (f g : BoundedContinuousFunction α R) => { toFun := fun (x : α) => f x * g x, continuous_toFun := , map_bounded' := } }
                                @[simp]
                                theorem BoundedContinuousFunction.coe_mul {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Mul R] [BoundedMul R] [ContinuousMul R] (f : BoundedContinuousFunction α R) (g : BoundedContinuousFunction α R) :
                                (f * g) = f * g
                                theorem BoundedContinuousFunction.mul_apply {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Mul R] [BoundedMul R] [ContinuousMul R] (f : BoundedContinuousFunction α R) (g : BoundedContinuousFunction α R) (x : α) :
                                (f * g) x = f x * g x
                                Equations
                                • BoundedContinuousFunction.instPow = { pow := fun (f : BoundedContinuousFunction α R) (n : ) => { toFun := fun (x : α) => f x ^ n, continuous_toFun := , map_bounded' := } }
                                theorem BoundedContinuousFunction.coe_pow {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Monoid R] [BoundedMul R] [ContinuousMul R] (n : ) (f : BoundedContinuousFunction α R) :
                                (f ^ n) = f ^ n
                                @[simp]
                                theorem BoundedContinuousFunction.pow_apply {α : Type u} [TopologicalSpace α] {R : Type u_2} [PseudoMetricSpace R] [Monoid R] [BoundedMul R] [ContinuousMul R] (n : ) (f : BoundedContinuousFunction α R) (x : α) :
                                (f ^ n) x = f x ^ n
                                Equations
                                Equations
                                • BoundedContinuousFunction.instCommMonoid = let __spread.0 := BoundedContinuousFunction.instMonoid; CommMonoid.mk
                                Equations
                                Equations
                                theorem BoundedContinuousFunction.norm_eq {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) :
                                f = sInf {C : | 0 C ∀ (x : α), f x C}

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

                                theorem BoundedContinuousFunction.norm_eq_of_nonempty {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) [h : Nonempty α] :
                                f = sInf {C : | ∀ (x : α), f x C}

                                When the domain is non-empty, we do not need the 0 ≤ C condition in the formula for ‖f‖ as a sInf.

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

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

                                theorem BoundedContinuousFunction.norm_le {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] {f : BoundedContinuousFunction α β} {C : } (C0 : 0 C) :
                                f C ∀ (x : α), f x C

                                The norm of a function is controlled by the supremum of the pointwise norms.

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

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

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

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

                                Equations
                                Instances For
                                  @[simp]
                                  theorem BoundedContinuousFunction.coe_ofNormedAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : αβ) (Hf : Continuous f) (C : ) (H : ∀ (x : α), f x C) :
                                  theorem BoundedContinuousFunction.norm_ofNormedAddCommGroup_le {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] {f : αβ} (hfc : Continuous f) {C : } (hC : 0 C) (hfC : ∀ (x : α), f x C) :

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

                                  Equations
                                  Instances For

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

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem BoundedContinuousFunction.coe_normComp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) :
                                      f.normComp = norm f

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

                                      Equations
                                      • =

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

                                      Equations
                                      @[simp]
                                      theorem BoundedContinuousFunction.coe_zsmulRec {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (z : ) :
                                      (zsmulRec (fun (x : ) (x_1 : BoundedContinuousFunction α β) => x x_1) z f) = z f
                                      Equations
                                      • BoundedContinuousFunction.instSMulInt = { smul := fun (n : ) (f : BoundedContinuousFunction α β) => { toContinuousMap := n f.toContinuousMap, map_bounded' := } }
                                      @[simp]
                                      theorem BoundedContinuousFunction.coe_zsmul {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (r : ) (f : BoundedContinuousFunction α β) :
                                      (r f) = r f
                                      @[simp]
                                      theorem BoundedContinuousFunction.zsmul_apply {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (r : ) (f : BoundedContinuousFunction α β) (v : α) :
                                      (r f) v = r f v
                                      Equations
                                      Equations
                                      Equations
                                      • BoundedContinuousFunction.instNormedAddCommGroup = let __src := BoundedContinuousFunction.instSeminormedAddCommGroup; NormedAddCommGroup.mk

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

                                      BoundedSMul (in particular, topological module) structure #

                                      In this section, if β is a metric space and a 𝕜-module whose addition and scalar multiplication are compatible with the metric structure, then we show that the space of bounded continuous functions from α to β inherits a so-called BoundedSMul structure (in particular, a ContinuousMul structure, which is the mathlib formulation of being a topological module), by using pointwise operations and checking that they are compatible with the uniform distance.

                                      instance BoundedContinuousFunction.instSMul {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] :
                                      Equations
                                      • BoundedContinuousFunction.instSMul = { smul := fun (c : 𝕜) (f : BoundedContinuousFunction α β) => { toContinuousMap := c f.toContinuousMap, map_bounded' := } }
                                      @[simp]
                                      theorem BoundedContinuousFunction.coe_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] (c : 𝕜) (f : BoundedContinuousFunction α β) :
                                      (c f) = fun (x : α) => c f x
                                      theorem BoundedContinuousFunction.smul_apply {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] (c : 𝕜) (f : BoundedContinuousFunction α β) (x : α) :
                                      (c f) x = c f x
                                      instance BoundedContinuousFunction.instIsCentralScalar {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] [SMul 𝕜ᵐᵒᵖ β] [IsCentralScalar 𝕜 β] :
                                      Equations
                                      • =
                                      instance BoundedContinuousFunction.instBoundedSMul {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [BoundedSMul 𝕜 β] :
                                      Equations
                                      • =
                                      Equations
                                      Equations
                                      instance BoundedContinuousFunction.instModule {α : Type u} {β : Type v} {𝕜 : Type u_2} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Semiring 𝕜] [AddCommMonoid β] [Module 𝕜 β] [BoundedSMul 𝕜 β] [BoundedAdd β] [ContinuousAdd β] :
                                      Equations
                                      • BoundedContinuousFunction.instModule = Function.Injective.module 𝕜 { toFun := DFunLike.coe, map_zero' := , map_add' := }
                                      def BoundedContinuousFunction.evalCLM {α : Type u} {β : Type v} (𝕜 : Type u_2) [PseudoMetricSpace 𝕜] [TopologicalSpace α] [PseudoMetricSpace β] [Semiring 𝕜] [AddCommMonoid β] [Module 𝕜 β] [BoundedSMul 𝕜 β] [BoundedAdd β] [ContinuousAdd β] (x : α) :

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

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

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

                                        Equations
                                        Instances For

                                          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.

                                          Equations

                                          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.
                                          Instances For
                                            @[simp]

                                            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.

                                            Equations
                                            Equations
                                            • BoundedContinuousFunction.instNonUnitalSeminormedRing = let __src := BoundedContinuousFunction.instSeminormedAddCommGroup; NonUnitalSeminormedRing.mk
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            @[simp]
                                            theorem BoundedContinuousFunction.coe_npowRec {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] (f : BoundedContinuousFunction α R) (n : ) :
                                            (npowRec n f) = f ^ n
                                            Equations
                                            • BoundedContinuousFunction.hasNatPow = { pow := fun (f : BoundedContinuousFunction α R) (n : ) => { toContinuousMap := f.toContinuousMap ^ n, map_bounded' := } }
                                            Equations
                                            @[simp]
                                            theorem BoundedContinuousFunction.coe_natCast {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] (n : ) :
                                            n = n
                                            @[simp]
                                            theorem BoundedContinuousFunction.coe_ofNat {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] (n : ) [n.AtLeastTwo] :
                                            (OfNat.ofNat n) = OfNat.ofNat n
                                            Equations
                                            @[simp]
                                            theorem BoundedContinuousFunction.coe_intCast {α : Type u} [TopologicalSpace α] {R : Type u_2} [SeminormedRing R] (n : ) :
                                            n = n
                                            Equations
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Equations
                                            • BoundedContinuousFunction.instNormedRing = let __spread.0 := BoundedContinuousFunction.instRing; let __spread.1 := BoundedContinuousFunction.instNonUnitalNormedRing; 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.

                                            Equations
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Equations
                                            • BoundedContinuousFunction.instNormedCommRing = let __spread.0 := BoundedContinuousFunction.instCommRing; let __spread.1 := BoundedContinuousFunction.instNormedAddCommGroup; NormedCommRing.mk

                                            Normed algebra structure #

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

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

                                            BoundedContinuousFunction.const as a RingHom.

                                            Equations
                                            Instances For
                                              instance BoundedContinuousFunction.instAlgebra {α : Type u} {γ : Type w} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] :
                                              Equations
                                              • BoundedContinuousFunction.instAlgebra = Algebra.mk BoundedContinuousFunction.C
                                              @[simp]
                                              theorem BoundedContinuousFunction.algebraMap_apply {α : Type u} {γ : Type w} {𝕜 : Type u_2} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] (k : 𝕜) (a : α) :
                                              ((algebraMap 𝕜 (BoundedContinuousFunction α γ)) k) a = k 1
                                              Equations
                                              • BoundedContinuousFunction.instNormedAlgebra = let __spread.0 := BoundedContinuousFunction.instAlgebra; let __spread.1 := BoundedContinuousFunction.instNormedSpace; 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 𝕜.

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

                                              Star structures #

                                              In this section, if β is a normed ⋆-group, then so is the space of bounded continuous functions from α to β, by using the star operation pointwise.

                                              If 𝕜 is normed field and a ⋆-ring over which β is a normed algebra and a star module, then the space of bounded continuous functions from α to β is a star module.

                                              If β is a ⋆-ring in addition to being a normed ⋆-group, then α →ᵇ β inherits a ⋆-ring structure.

                                              In summary, if β is a C⋆-algebra over 𝕜, then so is α →ᵇ β; note that completeness is guaranteed when β is complete (see BoundedContinuousFunction.complete).

                                              Equations
                                              @[simp]

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

                                              Equations
                                              • =
                                              Equations
                                              • BoundedContinuousFunction.instStarRing = let __spread.0 := BoundedContinuousFunction.instStarAddMonoid; StarRing.mk
                                              Equations
                                              Equations
                                              • BoundedContinuousFunction.instSup = { sup := fun (f g : BoundedContinuousFunction α β) => { toFun := f g, continuous_toFun := , map_bounded' := } }
                                              Equations
                                              • BoundedContinuousFunction.instInf = { inf := fun (f g : BoundedContinuousFunction α β) => { toFun := f g, continuous_toFun := , map_bounded' := } }
                                              @[simp]
                                              @[simp]
                                              Equations
                                              Equations
                                              Equations
                                              @[simp]
                                              @[deprecated BoundedContinuousFunction.coe_sup]

                                              Alias of BoundedContinuousFunction.coe_sup.

                                              @[deprecated BoundedContinuousFunction.coe_abs]

                                              Alias of BoundedContinuousFunction.coe_abs.

                                              Equations
                                              • BoundedContinuousFunction.instNormedLatticeAddCommGroup = let __src := BoundedContinuousFunction.instSeminormedAddCommGroup; NormedLatticeAddCommGroup.mk

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

                                              Equations
                                              Instances For

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

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem BoundedContinuousFunction.nnnorm_coeFn_eq {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ) :
                                                  f.nnnorm = nnnorm f

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

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