Inverse_of_Mapping_is_One_to_Many_Relation
Provedinverse-mappingsinverse-relationsproofwiki
Let f be a mapping. Then its inverse f⁻¹ is a one-to-many relation (unless f is injective).
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Inverse_of_Mapping_is_One_to_Many_Relation {α β : Type _} (f : α → β) (y : β) (x₁ x₂ : α) (h₁ : f x₁ = y) (h₂ : f x₂ = y) : ¬ Function.Injective f → ∃ a b : α, a ≠ b ∧ f a = f b := by sorrySource