card_setUniv — Mathlib

English

For a finite α, the cardinality of Set.univ equals the cardinality of α (under appropriate finiteness assumptions).

Русский

Для конечного α кардинал множества Set.univ равен кардиналу α (при соответствующих предпосылках).

LaTeX

$$$ \mathrm{card}( \mathrm{Set.univ} : \mathrm{Set} \alpha ) = \mathrm{card}( \alpha ) $$$

Lean4

@[simp]
theorem card_setUniv [Fintype α] {h : Fintype (Set.univ : Set α)} : Fintype.card (Set.univ : Set α) = Fintype.card α :=
  by
  apply Fintype.card_of_finset'
  simp

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