inclusion_range — Mathlib

English

If H ≤ K are subgroups of G, then the image of the natural inclusion i: H → K equals H viewed as a subgroup of K.

Русский

Если H ≤ K — подгруппы G, то образ естественного вложения i: H → K равен H, воспринятой как подгруппа K.

LaTeX

$$$$ \\mathrm{Im}(i_{H\\to K}) = H \\text{ (as a subgroup of } K) $$$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.Subgroup.inclusion_range {H K : Subgroup G} (h_le : H ≤ K) : (inclusion h_le).range = H.subgroupOf K :=
  Subgroup.ext fun g => Set.ext_iff.mp (Set.range_inclusion h_le) g

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