coe_ofNormedAddCommGroup — Mathlib

English

Let f: α → β be continuous and bounded by C, then the bounded continuous function obtained from f coincides with f itself. In other words, the canonical realization of f as a bounded continuous map equals f.

Русский

Пусть f: α → β бесконечно непрерывна и ограничена сверху константой C. Тогда каноническое отображение f в ограниченную непрерывную функцию совпадает с самой функцией f.

LaTeX

$$$\bigl(\text{ofNormedAddCommGroup } f\, H_f\, C\, H\bigr) = f$$$

Lean4

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

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