rank_closure_finite_le_nat_card — Mathlib

English

If s is a finite set, then rank(closure s) ≤ |s| in Nat-card terms: rank(closure s) ≤ card(s).

Русский

Если s — конечное множество, то rank(closure s) ≤ card(s).

LaTeX

$$$\forall s \subseteq G, \; [\text{Finite } s] \implies \operatorname{rank}(\overline{s}) \le \operatorname{card}(s).$$$

Lean4

@[to_additive]
theorem rank_closure_finite_le_nat_card (s : Set G) [Finite s] : rank (closure s) ≤ Nat.card s :=
  by
  haveI := Fintype.ofFinite s
  rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]
  exact rank_closure_finset_le_card s.toFinset

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