coe_toContinuousMapHom — Mathlib

English

The map coeFnAddMonoidHom embeds C(X, R)₀ into X → R as an additive monoid hom, i.e., it preserves zero and addition.

Русский

Встраивание coeFnAddMonoidHom инъективно отображает C(X, R)₀ как множество функций X → R и сохраняет ноль и сумму.

LaTeX

$$$\text{coeFnAddMonoidHom} : C(X, R)₀ \to^+ X \to R$$$

Lean4

theorem coe_toContinuousMapHom [StarRing R] [ContinuousStar R] : ⇑(toContinuousMapHom (X := X) (R := R)) = (↑) :=
  rfl

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