map_subtype_le_map_subtype — Mathlib

English

There is an order isomorphism between subgroups of H and subgroups of G lying inside H, given by taking the image under the inclusion H.subtype.

Русский

Существует упорядоченноеизм между подгруппами H и подгруппами G, лежащими внутри H, заданное отображением образа через включение H.subtype.

LaTeX

$$\\text{orderIso}(H) : \\operatorname{Subgroup} H \\cong_o \\{ H' \\le G : H' \\le H \\}$$

Lean4

@[to_additive (attr := simp)]
theorem map_subtype_le_map_subtype {G' : Subgroup G} {H K : Subgroup G'} :
    H.map G'.subtype ≤ K.map G'.subtype ↔ H ≤ K :=
  map_le_map_iff_of_injective G'.subtype_injective

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