nonempty_of_card_le — Mathlib

English

Let α and β be finite types. If |α| ≤ |β|, there exists an injective map f: α → β.

Русский

Пусть α и β — конечные множества. Если |α| ≤ |β|, существует инъекция f: α → β.

LaTeX

$$$|\alpha| \\le |\\beta| \\Rightarrow \\exists f:\\alpha \\to \\beta, \\operatorname{Injective}(f) $$$

Lean4

theorem nonempty_of_card_le [Fintype α] [Fintype β] (h : Fintype.card α ≤ Fintype.card β) : Nonempty (α ↪ β) := by
  classical exact (truncOfCardLE h).nonempty

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