comap_normalClosure — Mathlib

English

For a bijection f, the normalClosure of a preimage equals the comap of the normalClosure.

Русский

При биекции f нормальное замыкание предобраза равняется предобразу нормального замыкания.

LaTeX

$$$ \\operatorname{normalClosure}(\\mathrm{Set.preimage}(f, s)) = \\mathrm{comap}(f)(\\operatorname{normalClosure}(s)) $$$

Lean4

theorem comap_normalClosure (s : Set N) (f : G ≃* N) : normalClosure (f ⁻¹' s) = (normalClosure s).comap f :=
  by
  have := Set.preimage_equiv_eq_image_symm s f.toEquiv
  simp_all [comap_equiv_eq_map_symm, map_normalClosure s (f.symm : N →* G) f.symm.surjective]

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