of_coeHom_comp — Mathlib

English

Let f: G →* Hˣ be a monoid hom. If the composite (Units.coeHom H) ∘ f is continuous, then f is continuous.

Русский

Пусть f: G →* Hˣ — моноидная гомоморфия. Если композиция (Units.coeHom H) ∘ f непрерывна, тогда f непрерывна.

LaTeX

$$$ \\text{Continuous}(((Units.coeHom H) \\circ f)) \\Rightarrow \\text{Continuous}(f) $$$

Lean4

theorem of_coeHom_comp [Group G] [Monoid H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousInv G] {f : G →* Hˣ}
    (hf : Continuous ((Units.coeHom H).comp f)) : Continuous f :=
  by
  apply continuous_induced_rng.mpr ?_
  refine continuous_prodMk.mpr ⟨hf, ?_⟩
  simp_rw [← map_inv]
  exact MulOpposite.continuous_op.comp (hf.comp continuous_inv)

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