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

• orderIsoIooNegOneOne k = StrictMono.orderIsoOfRightInverse (Set.codRestrict (fun (x : k) => x / (1 + |x|)) (Set.Ioo (-1) 1) ⋯) ⋯ (fun (x : ↑(Set.Ioo (-1) 1)) => ↑x / (1 - |↑x|)) ⋯