mathlib documentation


Order isomorphism between a linear ordered field and (-1, 1) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we provide an order isomorphism order_iso_Ioo_neg_one_one between the open interval (-1, 1) in a linear ordered field and the whole field.


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.