continuous_comp_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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