Composite_of_Bijection_with_Inverse_is_Identity_Mapping
Provedbijectionsinverse-mappingsproofwiki
Let f: S → T be a bijection. Then f⁻¹ ∘ f = I_S and f ∘ f⁻¹ = I_T.
Preamble
import Mathlib.Logic.Equiv.Basic
Formal statement
theorem Composite_of_Bijection_with_Inverse_is_Identity_Mapping {α β : Type _} (f : α ≃ β) : f.symm ∘ f = id ∧ f ∘ f.symm = id := by sorrySource