subtype_card — Mathlib

English

For p : α → Prop and s : Finset α with H: ∀ x, x ∈ s ↔ p x, the cardinality of the subtype {x // p x} equals the cardinality of s.

Русский

Для p : α → Prop и s : Finset α с условием H: ∀ x, x ∈ s ⇔ p x, кардинал субтипа {x // p x} равен кардиналу s.

LaTeX

$$$ \\#\\{ x : α \\mid p x \\} = \\#s.$$$

Lean4

theorem subtype_card {p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ s ↔ p x) :
    @card { x // p x } (Fintype.subtype s H) = #s :=
  Multiset.card_pmap _ _ _

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