card_embedding_eq_of_unique — Mathlib

English

If α has a unique element (Unique α) and β is finite, then the embeddings α ↪ β are in one-to-one correspondence with elements of β; hence |α ↪ β| = |β|.

Русский

Если α имеет один элемент (Unique α), а β — конечен, то множество вложений α ↪ β эквивалентно β; следовательно, |α ↪ β| = |β|.

LaTeX

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

Lean4

theorem card_embedding_eq_of_unique {α β : Type*} [Unique α] [Fintype β] [Fintype (α ↪ β)] : ‖α ↪ β‖ = ‖β‖ :=
  card_congr Equiv.uniqueEmbeddingEquivResult

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