Inverse_of_Bijection_is_Bijection
Provedbijectionsinverse-mappingsproofwiki
Let f: S → T be a bijection. Then the inverse f⁻¹ of f is itself a bijection.
Preamble
import Mathlib.Logic.Equiv.Basic
Formal statement
theorem Inverse_of_Bijection_is_Bijection {α β : Type _} (f : α ≃ β) : Function.Bijective f.symm := by sorrySource