card_subtype_mono — Mathlib

English

If p ≤ q are predicates on α, then the cardinality of the p-subtype is at most the cardinality of the q-subtype, i.e., |{x // p x}| ≤ |{x // q x}|.

Русский

Если p ≤ q, то кардинальность подтипа p не превосходит кардинальность подтипа q.

LaTeX

$$$|\{ x // p x \}| \le |\{ x // q x \}|$$$

Lean4

theorem card_subtype_mono (p q : α → Prop) (h : p ≤ q) [Fintype { x // p x }] [Fintype { x // q x }] :
    Fintype.card { x // p x } ≤ Fintype.card { x // q x } :=
  Fintype.card_le_of_embedding (Subtype.impEmbedding _ _ h)

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