English
If H ≤ K are subgroups of G, the natural equivalence between H viewed as a subgroup of K and H remains the same via the subgroupOf construction; i.e., H viewed inside K is the same as H as a subgroup of G restricted to K.
Русский
Если H ≤ K — подгруппы G, естественное биекция между H как подгруппой K и H как подгруппой G не меняется через конструкцию subgroupOf.
LaTeX
$$$ H \\text{ subgroupOf } K \\; \\cong\\; H $$$
Lean4
/-- If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`. -/
@[to_additive (attr := simps) /-- If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`. -/
]
def subgroupOfEquivOfLe {G : Type*} [Group G] {H K : Subgroup G} (h : H ≤ K) : H.subgroupOf K ≃* H
where
toFun g := ⟨g.1, g.2⟩
invFun g := ⟨⟨g.1, h g.2⟩, g.2⟩
map_mul' _g _h := rfl
