Direct_Image_Mapping_is_Bijection_iff_Mapping_is_Bijection
Provedbijectionsdirect-image-mappingsproofwiki
A mapping f is a bijection if and only if its direct image mapping is a bijection.
Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem Direct_Image_Mapping_is_Bijection_iff_Mapping_is_Bijection {α : Type _} {β : Type _} (f : α → β) : Function.Bijective f ↔ Function.Bijective (Set.image f) := by sorrySource