subtype_card — Mathlib

English

For a Finset s and predicate p with H: ∀ x, x ∈ s ↔ p x, the cardinality of the subtype { x // p x } equals Finset.card s.

Русский

Пусть s — конечный набор и p — предикат с условием H: ∀ x, x ∈ s ↔ p x. Тогда Nat.card { x // p x } = Finset.card s.

LaTeX

$$$ \forall p : \alpha \to \mathrm{Prop}, \forall s : \mathrm{Finset}\,\alpha, ( \forall x, x \in s \leftrightarrow p x) \rightarrow \mathrm{Nat.card}\{ x // p x \} = \mathrm{Finset.card}\,s $$$

Lean4

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

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