embeddingEquivOfFinite — Mathlib

English

On a finite type, there is a natural equivalence between self-embeddings and bijections.

Русский

На конечном типе существует естественное сопоставление между самовстраиваемостями и биекциям.

LaTeX

$$$\\text{Equiv.embeddingEquivOfFinite}: (\\alpha \\to \\alpha) \\simeq (\\alpha \\simeq \\alpha)$$$

Lean4

/-- On a finite type, equivalence between the self-embeddings and the bijections. -/
@[simps]
noncomputable def _root_.Equiv.embeddingEquivOfFinite (α : Type*) [Finite α] : (α ↪ α) ≃ (α ≃ α)
    where
  toFun e := e.equivOfFiniteSelfEmbedding
  invFun e := e.toEmbedding

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