Commit 2026-11-10 14:10 218951eb

feat(Logic/Relation,Order/WellFounded): lemmas about Acc, WellFounded, and Relation.Map (#44696)

• Acc (Relation.Map r f f) (f a) and WellFounded (Relation.Map r f f) imply Acc r a and WellFounded r respectively;
• They are equivalent respectively if f is injective. Suggested by @plp127 in https://github.com/leanprover-community/mathlib4/pull/39774#discussion_r3618397529