units_map — Mathlib

English

If f: M →* N is a monoid hom and continuous, then the induced map on units Units.map f is continuous.

Русский

Если f: M →* N — гомоморфизм моноидов и непрерывен, то сопряженная карта Units.map f непрерывна.

LaTeX

$$$\\text{Continuous (MonoidHom.coe) } \\Rightarrow \\text{Continuous (MonoidHom.coe) (Units.map f)}$$$

Lean4

@[to_additive (attr := fun_prop)]
theorem units_map [Monoid M] [Monoid N] [TopologicalSpace M] [TopologicalSpace N] (f : M →* N) (hf : Continuous f) :
    Continuous (Units.map f) :=
  Units.continuous_iff.2 ⟨hf.comp Units.continuous_val, hf.comp Units.continuous_coe_inv⟩

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