topologicalGroup_induced — Mathlib

English

Let f be a map with the appropriate algebraic structure; the induced topology on H makes H a topological group if the relevant conditions hold.

Русский

Пусть имеется отображение с необходимой алгебраической структурой; индуцированная по нему топология на H делает H топологической группой при выполнении условий.

LaTeX

$$$IsTopologicalGroup(H,\ \text{induced } f)$$$

Lean4

@[to_additive]
theorem topologicalGroup_induced {F : Type*} [Group H] [FunLike F H G] [MonoidHomClass F H G] (f : F) :
    @IsTopologicalGroup H (induced f ‹_›) _ :=
  letI := induced f ‹_›
  IsInducing.topologicalGroup f ⟨rfl⟩

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