Inverse_Element_of_Bijection
Provedbijectionsinverse-mappingsproofwiki
Let S and T be sets. Let f: S → T be a bijection. Then f⁻¹(y) = x ↔ f(x) = y.
Preamble
import Mathlib.Logic.Equiv.Basic
Formal statement
theorem Inverse_Element_of_Bijection {α β : Type _} (f : α ≃ β) (x : α) (y : β) : f.symm y = x ↔ f x = y := by sorrySource