coe_toContinuousMapₐ — Mathlib

English

There is a forgetful map from bounded continuous functions to continuous maps that preserves the underlying function and the algebraic structure.

Русский

Существует отображение забывания от ограниченных непрерывных функций к непрерывным отображениям, сохраняющее базовую функцию и алгебраическую структуру.

LaTeX

$$$\\text{toContinuousMap}_{\\mathcal{A}}: (α \\to^b γ) \\to_a (C(α, γ))$ is compatible with coefficients.$$

Lean4

@[simp]
theorem coe_toContinuousMapₐ (f : α →ᵇ γ) : (f.toContinuousMapₐ 𝕜 : α → γ) = f :=
  rfl

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