irreflexive relations on a unique type are isomorphic (#14760)

Commit

3 years ago

feat(order/rel_iso): two reflexive/irreflexive relations on a unique type are isomorphic (#14760) We also rename `not_rel` to the more descriptive name `not_rel_of_subsingleton`.

Author

vihdzp

Parents

6df59d68

mathlib 691f04fe - feat(order/rel_iso): two reflexive/irreflexive relations on a unique type are isomorphic (#14760)

mathlib
691f04fe - feat(order/rel_iso): two reflexive/irreflexive relations on a unique type are isomorphic (#14760)