English
For nonempty α, |FreeGroup α| = max(|α|, ℵ0).
Русский
Для непустого α выполняется |FreeGroup α| = max(|α|, ℵ0).
LaTeX
$$$\\lvert \\mathrm{FreeGroup}(\\alpha) \\rvert = \\max\\{|\\alpha|, \\aleph_0\\}$$$
Lean4
@[to_additive (attr := simp)]
theorem mk_freeGroup [Nonempty α] : #(FreeGroup α) = max #α ℵ₀ := by
classical
apply le_antisymm
· apply (mk_le_of_injective (FreeGroup.toWord_injective (α := α))).trans_eq
simp [Cardinal.mk_list_eq_max_mk_aleph0]
obtain hα | hα := lt_or_ge #α ℵ₀
· simp only [hα.le, max_eq_right, max_eq_right_iff]
exact (mul_lt_aleph0 hα (nat_lt_aleph0 2)).le
· rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
Cardinal.mul_eq_left hα _ (by simp)]
exact (nat_lt_aleph0 2).le.trans hα
· apply max_le
· exact mk_le_of_injective FreeGroup.of_injective
· simp
