card_embedding_eq_of_infinite — Mathlib

English

If α is infinite and β is finite, there are no embeddings α ↪ β; equivalently, |α ↪ β| = 0.

Русский

Если α бесконечен, а β конечен, то вложений α ↪ β не существует; значит, |α ↪ β| = 0.

LaTeX

$$$$ |\alpha \hookrightarrow \beta| = 0 $$$$

Lean4

/-- The cardinality of embeddings from an infinite type to a finite type is zero.
This is a re-statement of the pigeonhole principle. -/
theorem card_embedding_eq_of_infinite {α β : Type*} [Infinite α] [Finite β] [Fintype (α ↪ β)] : ‖α ↪ β‖ = 0 :=
  card_eq_zero

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