continuous_comp — Mathlib

English

The map sending a pair of continuous monoid homomorphisms to their composition is continuous (under LocallyCompactSpace B).

Русский

Отображение, отправляющее пару непрерывных моноидных гомоморфизмов в их композицию, непрерывно (при LocallyCompactSpace B).

LaTeX

$$$[LocallyCompactSpace B] \Rightarrow \; (f,g) \mapsto g \circ f \,\text{ is continuous}.$$$

Lean4

@[to_additive]
theorem continuous_comp [LocallyCompactSpace B] :
    Continuous fun f : ContinuousMonoidHom A B × ContinuousMonoidHom B C => f.2.comp f.1 :=
  (isInducing_toContinuousMap A C).continuous_iff.2 <|
    ContinuousMap.continuous_comp'.comp
      ((isInducing_toContinuousMap A B).prodMap (isInducing_toContinuousMap B C)).continuous

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