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