Inclusion_Mapping_is_Injection
Provedinclusion-mappingsinjectionsproofwiki
Let S, T be sets such that S is a subset of T. Then the inclusion mapping i_S: S → T is an injection.
Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem Inclusion_Mapping_is_Injection {α : Type _} {S T : Set α} (h : S ⊆ T) : Function.Injective (Set.inclusion h) := by sorrySource