equivOfFiniteSelfEmbedding — Mathlib

English

An embedding from a finite type into itself can be promoted to a bijection.

Русский

Встраивание типа в себя можно превратить в биективное соответствие.

LaTeX

$$$\\text{Equiv.Embedding.equivOfFiniteSelfEmbedding}: (α \\hookrightarrow α) \\to (\\alpha \\simeq \\alpha)$$$

Lean4

/-- An embedding from a `Fintype` to itself can be promoted to an equivalence. -/
noncomputable def equivOfFiniteSelfEmbedding [Finite α] (e : α ↪ α) : α ≃ α :=
  Equiv.ofBijective e e.2.bijective_of_finite

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