English
The rank of the closure of the commutator representatives is bounded by twice the number of commutators: rank(closureCommutatorRepresentatives(G)) ≤ 2 · card(commutatorSet(G)).
Русский
Ранг замыкания коммутаторов не превосходит удвоенного количества коммутаторов: rank(closureCommutatorRepresentatives(G)) ≤ 2 · card(commutatorSet(G)).
LaTeX
$$$\mathrm{rank}(\mathrm{closureCommutatorRepresentatives}(G)) \le 2 \cdot \mathrm{card}(\mathrm{commutatorSet}(G))$$$
Lean4
theorem rank_closureCommutatorRepresentatives_le :
Group.rank (closureCommutatorRepresentatives G) ≤ 2 * Nat.card (commutatorSet G) :=
by
rw [two_mul]
exact
(Subgroup.rank_closure_finite_le_nat_card _).trans
((Set.card_union_le _ _).trans
(add_le_add ((Finite.card_image_le _).trans (Finite.card_range_le _))
((Finite.card_image_le _).trans (Finite.card_range_le _))))
