ofNormedAddCommGroupDiscrete — Mathlib

English

On a discrete space α, every bounded function f: α → β determines a bounded continuous function with the same underlying map.

Русский

На дискретном пространстве α любая ограниченная функция f: α → β задаёт ограниченную непрерывную функцию с тем же отображением.

LaTeX

$$$(\text{ofNormedAddCommGroupDiscrete } f\, C\, H) = f$$$

Lean4

/-- Constructing a bounded continuous function from a uniformly bounded
function on a discrete space, taking values in a normed group. -/
def ofNormedAddCommGroupDiscrete {α : Type u} {β : Type v} [TopologicalSpace α] [DiscreteTopology α]
    [SeminormedAddCommGroup β] (f : α → β) (C : ℝ) (H : ∀ x, norm (f x) ≤ C) : α →ᵇ β :=
  ofNormedAddCommGroup f continuous_of_discreteTopology C H

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