toContinuousMap_toContinuousMonoidHom

English

The underlying continuous map of the continuous monoid homomorphism f is f itself.

Русский

Неявное отображение непрерывной функции-моноид-гомоморфизма f есть сама функция f.

LaTeX

$$$((f : A \\to_{}^* B) : C(A,B))= f$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem toContinuousMap_toContinuousMonoidHom [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) :
    ((f : A →ₜ* B) : C(A, B)) = f :=
  rfl

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