comap — Mathlib

English

The preimage of an open subgroup under a continuous monoid homomorphism is an open subgroup.

Русский

Предобраз открытой подгруппы по непрерывному моноидному однородному отображению является открытой подгруппой.

LaTeX

$$$$ H^{\\mathrm{comap}(f,hf)} \\text{ is an open subgroup of } G. $$$$

Lean4

/-- The preimage of an `OpenSubgroup` along a continuous `Monoid` homomorphism
  is an `OpenSubgroup`. -/
@[to_additive /-- The preimage of an `OpenAddSubgroup` along a continuous `AddMonoid` homomorphism
    is an `OpenAddSubgroup`. -/
    ]
def comap (f : G →* N) (hf : Continuous f) (H : OpenSubgroup N) : OpenSubgroup G :=
  ⟨.comap f H, H.isOpen.preimage hf⟩

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