instCoeOutOfMonoidHomClassOfContinuousMapClass

English

If F consists of objects that are monoid homomorphisms A → B and continuous maps A → B, then there is a canonical coercion from F to the type of continuous monoid homomorphisms A →ₜ* B.

Русский

Если F состоит из объектов, которые являются моноид-гомоморфизмами A → B и непрерывными отображениями A → B, существует каноническое приведение F к типу непрерывных моноид-гомоморфизмов A →* B.

LaTeX

$$$\\text{CoeOut from } F \\ to \\ (A \\to_{}^* B)$$$

Lean4

/-- Any type satisfying `MonoidHomClass` and `ContinuousMapClass` can be cast into
`ContinuousMonoidHom` via `ContinuousMonoidHom.toContinuousMonoidHom`. -/
@[to_additive /-- Any type satisfying `AddMonoidHomClass` and `ContinuousMapClass` can be cast into
    `ContinuousAddMonoidHom` via `ContinuousAddMonoidHom.toContinuousAddMonoidHom`. -/
    ]
instance [MonoidHomClass F A B] [ContinuousMapClass F A B] : CoeOut F (A →ₜ* B) :=
  ⟨ContinuousMonoidHom.toContinuousMonoidHom⟩

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