mk_subtype_mono — Mathlib

English

If p implies q for predicates on α, then the cardinality of the subtype {x | p x} is less than or equal to the cardinality of {x | q x}.

Русский

Если p(x) ⇒ q(x) для всех x в α, то кардинал подтипа {x | p x} не превосходит кардинал {x | q x}.

LaTeX

$$$\#\{ x \;\//\; p x \} \leq \#\{ x \;\//\; q x \}$$$

Lean4

theorem mk_subtype_mono {p q : α → Prop} (h : ∀ x, p x → q x) : #{ x // p x } ≤ #{ x // q x } :=
  ⟨embeddingOfSubset _ _ h⟩

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