continuous_comp_right — Mathlib

English

The map f ↦ f ∘ g is continuous for a fixed g: B → C, under LocallyCompactSpace B.

Русский

Для фиксированного g: B → C функция f ↦ f ∘ g непрерывна при LocallyCompactSpace B.

LaTeX

$$$\text{Continuous}(\mathrm{ContinuousMonoidHom}\, A\, B) \Rightarrow \; f \mapsto f \circ g\text{ is continuous}.$$$

Lean4

@[to_additive]
theorem continuous_comp_right (f : ContinuousMonoidHom B C) : Continuous fun g : ContinuousMonoidHom A B => f.comp g :=
  (isInducing_toContinuousMap A C).continuous_iff.2 <|
    f.toContinuousMap.continuous_postcomp.comp (isInducing_toContinuousMap A B).continuous

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