Injectivity on a union and invariant sets of injective maps

• Set.InjOn.union_of_disjoint_image: a map injective on two sets with disjoint images is injective on their union.
• Function.Injective.mapsTo_of_eq_self: an injective self-map fixing every point outside a set K maps K into itself.

theorem Set.InjOn.union_of_disjoint_image {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set α} (hs : InjOn f s) (ht : InjOn f t) (h : Disjoint (f '' s) (f '' t)) : InjOn f (s ∪ t)

A map injective on two sets whose images are disjoint is injective on their union.

theorem Function.Injective.mapsTo_of_eq_self {α : Type u_1} {f : α → α} (hf : Injective f) {K : Set α} (h : ∀ (p : α), ¬p ∈ K → f p = p) : Set.MapsTo f K K

An injective map fixing every point outside K maps K into itself.