card_subtype — Mathlib

English

The cardinality of the subtype {x // p x} equals the cardinality of the Finset of elements of univ that satisfy p, i.e., the number of x with p(x).

Русский

Кардинальность подтипа {x // p x} равна кардинальности множества, полученного фильтрацией универсума по p, то есть числу элементов, удовлетворяющих p.

LaTeX

$$$\#\{ x // p x \} = \#(\mathrm{Finset.filter} (\lambda x, p x) \mathrm{Finset.univ})$$$

Lean4

theorem card_subtype [Fintype α] (p : α → Prop) [Fintype { a // p a }] [DecidablePred p] :
    Fintype.card { x // p x } = #{x | p x} :=
  by
  refine Fintype.card_of_subtype _ ?_
  simp

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