card_of_subtype — Mathlib

English

Let s be a finite set of α and p a predicate with H: ∀ x, x ∈ s ↔ p x. If there is a Finite type for the subtype {x // p x}, then Fintype.card { x // p x } = s.card.

Русский

Пусть s — конечное подмножество α и p предикат с H: ∀ x, x ∈ s ⇔ p x. Если существует конечный тип для подтипа {x // p x}, то Fintype.card { x // p x } = s.card.

LaTeX

$$$ \\operatorname{card} \\{ x : α \\mid p x \\} = |s|.$$$

Lean4

theorem card_of_subtype {p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ s ↔ p x) [Fintype { x // p x }] :
    card { x // p x } = #s := by
  rw [← subtype_card s H]
  congr!

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