Order isomorphism between a linear ordered field and
(-1, 1) #
In this file we provide an order isomorphism
orderIsoIooNegOneOne between the open interval
(-1, 1) in a linear ordered field and the whole field.
def orderIsoIooNegOneOne (k : Type u_1) [inst : LinearOrderedField k] :
In a linear ordered field, the whole field is order isomorphic to the open interval
We consider the actual implementation to be a "black box", so it is irreducible.
- One or more equations did not get rendered due to their size.