ncard_coe_finset — Mathlib

English

For every finite α and every finite set s represented as a Finset α, the cardinality of the set corresponding to s equals the Finset's own cardinality: ncard of the underlying set equals card(s).

Русский

Для любого конечного типа α и для каждого Finset α, кардинал множества, порождаемого этим Finset, равен кардиналу самого Finset.

LaTeX

$$$ (s : Set \alpha).ncard = s.card $$$

Lean4

@[simp, norm_cast]
theorem ncard_coe_finset (s : Finset α) : (s : Set α).ncard = s.card := by
  rw [ncard_eq_toFinset_card _, Finset.finite_toSet_toFinset]

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