English
For any Finset S ⊆ G, rank(closure S) ≤ |S|.
Русский
Для любого конечного множества S ⊆ G, rank(closure(S)) ≤ |S|.
LaTeX
$$$\forall S \in \mathrm{Finset}(G),\ \operatorname{rank}(\overline{S}) \le |S|.$$$
Lean4
@[to_additive]
theorem rank_closure_finset_le_card (s : Finset G) : rank (closure (s : Set G)) ≤ s.card := by
classical
let t : Finset (closure (s : Set G)) := s.preimage Subtype.val Subtype.coe_injective.injOn
have ht : closure (t : Set (closure (s : Set G))) = ⊤ :=
by
rw [Finset.coe_preimage]
exact closure_preimage_eq_top (s : Set G)
apply (rank_le ht).trans
suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G)))
by
rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
apply Finset.card_filter_le
apply Subtype.coe_injective.injOn
