mk_finset_of_infinite — Mathlib

English

For infinite α, the cardinality of Finset α equals the cardinality of α.

Русский

Для бесконечного α кардинальность конечного множества α равна кардинальности α.

LaTeX

$$$|\\mathrm{Finset}(\\alpha)| = |\\alpha|$$$

Lean4

@[simp]
theorem mk_finset_of_infinite (α : Type u) [Infinite α] : #(Finset α) = #α := by
  classical
    exact
    Eq.symm <|
      le_antisymm (mk_le_of_injective fun _ _ => Finset.singleton_inj.1) <|
        calc
          #(Finset α) ≤ #(List α) := mk_le_of_surjective List.toFinset_surjective
          _ = #α := mk_list_eq_mk α

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