card_subtype_le — Mathlib

English

For any predicate p on α, the set of elements x with p(x) true forms a subtype whose cardinality does not exceed the cardinality of α; i.e., |{x ∈ α : p(x)}| ≤ |α|.

Русский

Для любого предиката p на α множество элементов x, удовлетворяющих p(x), имеет кардинальность не более кардинальности α; то есть |{x : p(x)}| ≤ |α|.

LaTeX

$$$|\{ x \mid p(x) \}| \le |\alpha|$$$

Lean4

theorem card_subtype_le [Fintype α] (p : α → Prop) [Fintype { a // p a }] :
    Fintype.card { x // p x } ≤ Fintype.card α :=
  Fintype.card_le_of_embedding (Function.Embedding.subtype _)

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