continuous_map — Mathlib

English

If f: M →* N is a continuous monoid homomorphism, then the induced map map f: Mˣ → Nˣ is continuous.

Русский

Если f: M →* N непрерывно, тогда отображение map f: Mˣ → Nˣ непрерывно.

LaTeX

$$$\\text{Continuous}(f) \\Rightarrow \\text{Continuous}(\\mathrm{map} f)$$$

Lean4

@[to_additive]
theorem continuous_map {f : M →* N} (hf : Continuous f) : Continuous (map f) :=
  Units.continuous_iff.mpr ⟨hf.comp continuous_val, hf.comp continuous_coe_inv⟩

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