mathlib

9d42f6c6 - feat(order/rel_iso): define `rel_hom` (relation-preserving maps) (#3946)

feat(order/rel_iso): define `rel_hom` (relation-preserving maps) (#3946) Creates a typeclass for (unidirectionally) relation-preserving maps that are not necessarily injective (In the case of <= relations, this is essentially a bundled monotone map) Proves that these transfer well-foundedness between relations