mk_subtype_le_of_subset — Mathlib

English

If p and q are predicates on α with p(x) ⇒ q(x) for all x, then |Subtype p| ≤ |Subtype q|.

Русский

Пусть p и q — предикаты на α, и p(x) ⇒ q(x) для всех x. Тогда кардинальность Subtype p не превосходит кардинальность Subtype q.

LaTeX

$$$|\\mathrm{Subtype}(p)| \\le |\\mathrm{Subtype}(q)|$$$

Lean4

theorem mk_subtype_le_of_subset {α : Type u} {p q : α → Prop} (h : ∀ ⦃x⦄, p x → q x) : #(Subtype p) ≤ #(Subtype q) :=
  ⟨Embedding.subtypeMap (Embedding.refl α) h⟩

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