Theorems · Definition · functional analysis

BoundedContinuousFunction.ofNormedAddCommGroupDiscrete

{α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [DiscreteTopology α] →
        [inst_2 : SeminormedAddCommGroup β] →
          (f : α → β) → (C : ℝ) → (∀ (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.

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Normed

Cited by

1 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceDiscreteTopologySeminormedAddCommGroup