card_of_finset' — Mathlib

English

A variant of card_ofFinset with a primed statement, confirming equality of finset card with fintype card under equivalence.

Русский

Вариант card_ofFinset c апострофом, подтверждающий равенство кардинала финсет и кардинала типа подстановки при эквивалентности.

LaTeX

$$$ \\operatorname{card}(p) = |s| \\quad (\\text{при } p(x) \\Leftrightarrow x \\in s). $$$

Lean4

theorem card_of_finset' {p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) [Fintype p] : Fintype.card p = #s := by
  rw [← card_ofFinset s H]; congr!

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