isCoatom_comap — Mathlib

English

Let f: G ≅* H be a group isomorphism and K a subgroup of H. Then K is a coatom in H if and only if its preimage comap under f is a coatom in G.

Русский

Пусть f: G ≅* H — изоморфизм групп, и K — подпгруппа H. Тогда K является коатомом в H тогда и только тогда, когда ее образ-предобраз под f является коатомом в G.

LaTeX

$$IsCoatom(K) \iff IsCoatom( Subgroup.comap (f : G →* H) K )$$

Lean4

@[simp]
theorem isCoatom_comap {H : Type*} [Group H] (f : G ≃* H) {K : Subgroup H} :
    IsCoatom (Subgroup.comap (f : G →* H) K) ↔ IsCoatom K :=
  OrderIso.isCoatom_iff (f.comapSubgroup) K

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