feat(logic/function/basic): add lemma stating that dite of two injective functions is injective if images are disjoint (#5866)
feat(logic/function/basic): add lemma stating that dite of two injective functions is injective if images are disjoint (#5866)

Add lemma stating that dite of two injective functions is injective if their images are disjoint. Part of #5695 in order to prove Hall's Marriage Theorem.



Co-authored-by: agusakov <067de2d7f4f5809454de1022e9c3aab9efe72888@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib