nonempty_iff_card_le — Mathlib

English

For finite α,β, there exists an embedding α ↪ β if and only if |α| ≤ |β|.

Русский

Пусть α,β конечны. Существует вложение α ↪ β тогда и только тогда, когда |α| ≤ |β|.

LaTeX

$$$\\operatorname{Nonempty}(\\alpha \\hookrightarrow \\beta) \\iff |\\alpha| \\le |\\beta|$$$

Lean4

theorem nonempty_iff_card_le [Fintype α] [Fintype β] : Nonempty (α ↪ β) ↔ Fintype.card α ≤ Fintype.card β :=
  ⟨fun ⟨e⟩ => Fintype.card_le_of_embedding e, nonempty_of_card_le⟩

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