Identity_Mapping_is_Permutation
Provedidentity-mappingspermutation-theoryproofwiki
The identity mapping I_S: S → S on the set S is a permutation (i.e., a bijection from S to itself).
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Identity_Mapping_is_Permutation {α : Type _} : Function.Bijective (id : α → α) := by sorrySource