ofNormedAddCommGroup — Mathlib

English

Construct a bounded continuous function from a boundedly valued function in a normed additive group; given a function f: α → β which is continuous and bounded by C, produce an α →ᵇ β.

Русский

Сконструировать ограниченно непрерывную функцию из функции, значений в нормированную аддитивную группу; если f: α → β непрерывна и ограничена по модулю, получаем элемент α →ᵇ β.

LaTeX

$$$ofNormedAddCommGroup:\\ α\\to β \\to\\text{BoundedContinuousFunction}(α,β)$$$

Lean4

/-- Constructing a bounded continuous function from a uniformly bounded continuous
function taking values in a normed group. -/
def ofNormedAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : α → β)
    (Hf : Continuous f) (C : ℝ) (H : ∀ x, ‖f x‖ ≤ C) : α →ᵇ β :=
  ⟨⟨fun n => f n, Hf⟩, ⟨_, dist_le_two_norm' H⟩⟩

Похожие утверждения