Order homomorphisms and sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Order isomorphism between two equal sets.
Order isomorphism between
univ : set α and
If a function
f is strictly monotone on a set
s, then it defines an order isomorphism
s and its image.
A strictly monotone function from a linear order is an order isomorphism between its domain and
A strictly monotone surjective function from a linear order is an order isomorphism.
Taking complements as an order isomorphism to the order dual.