feat(Order/RelIso/Basic): lift a function to an order morphism into Relation.Map or from Function.onFun

[SnirBroshi]

For an α-relation r we have:

mapRelHom       (f : α → β) : r →r Relation.Map r f f
mapRelEmbedding (f : α ↪ β) : r ↪r Relation.Map r f f
mapRelIso       (f : α ≃ β) : r ≃r Relation.Map r f f

For a β-relation r we have:

onFunRelHom       (f : α → β) : r.onFun f →r r
onFunRelEmbedding (f : α ↪ β) : r.onFun f ↪r r
onFunRelIso       (f : α ≃ β) : r.onFun f ≃r r

---

These are pretty similar to SimpleGraph.{Embedding/Iso}.map and SimpleGraph.{Hom/Embedding/Iso}.comap, as comap on graphs is a wrapper around onFun, and map on graphs is almost a wrapper around Relation.Map.

btw @[simps] is angry at me when I try to use it on the structures that use spread syntax.

[github-actions]

PR summary def28638ef

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ mapRelEmbedding
+ mapRelHom
+ mapRelIso
+ onFunRelEmbedding
+ onFunRelHom
+ onFunRelIso

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).