card_ofFinset — Mathlib

English

For p : Set α and s : Finset α with H: ∀ x, x ∈ s ↔ x ∈ p, the card of p’s fintype equals s.card.

Русский

Для p : Set α и s : Finset α с H: ∀ x, x ∈ s ⇔ x ∈ p, кардинал fintype p равен s.card.

LaTeX

$$$ \\operatorname{card} p = |s|, \\quad p(x) \\Leftrightarrow x \\in s.$$$

Lean4

@[simp]
theorem card_ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : @Fintype.card p (ofFinset s H) = #s :=
  Fintype.subtype_card s H

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