coe_comap — Mathlib

English

As sets, the comapped open subgroup equals the preimage under f: (H.comap f hf : Set G) = f^{-1}(H).

Русский

Как множества, открытая подгруппа после прообразования по f равна предобразованию: (H.comap f hf : Set G) = f^{-1}(H).

LaTeX

$$$$ (H^{\\mathrm{comap} f hf} : \\mathrm{Set} G) = f^{-1} H. $$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_comap (H : OpenSubgroup N) (f : G →* N) (hf : Continuous f) : (H.comap f hf : Set G) = f ⁻¹' H :=
  rfl

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