Documentation

Mathlib.Data.Set.Intervals.IsoIoo

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.

source
ink
def orderIsoIooNegOneOne (k : Type u_1) [inst : 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.