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.

@[irreducible]

def orderIsoIooNegOneOne (k : Type u_1) [LinearOrderedField k] : k ≃o ↑(Set.Ioo (-1) 1)

In a linear ordered field, the whole field is order isomorphic to the open interval (-1, 1). We consider the actual implementation to be a "black box", so it is irreducible.

Equations

• One or more equations did not get rendered due to their size.