mathlib3 documentation

data.set.intervals.iso_Ioo

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.

source
@[irreducible]
def order_iso_Ioo_neg_one_one (k : Type u_1) [linear_ordered_field 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