Inclusion_Mapping_is_Surjection_iff_Identity
Provedinclusion-mappingsproofwikisurjections
Let T be a set. Let S be a subset of T. The inclusion mapping from S to T is surjective iff it is the identity mapping.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Inclusion_Mapping_is_Surjection_iff_Identity {S T : Type _} (h : S -> T) (hinj : Function.Injective h) : Function.Surjective h <-> Function.Bijective h := by sorrySource