# Zulip Chat Archive

## Stream: maths

### Topic: Different linear orders on reals

#### Anatole Dedecker (Feb 13 2021 at 17:43):

It seems that `@conditionally_complete_linear_order.to_linear_order ℝ real.conditionally_complete_linear_order`

is not defeq with `real.linear_order`

, which seems strange since `real.conditionally_complete_linear_order`

is defined in terms of `real.linear_order`

.

Here is an example where it causes a problem : I have a proof of the intermediate value theorem for intervals, and the definition of `interval`

requires a `linear_order`

instance. So the following fails, because I'm mixing two different notions of `interval`

on `ℝ`

.

```
import analysis.special_functions.trigonometric
open set real
lemma intermediate_value_interval {α : Type*} [conditionally_complete_linear_order α]
[densely_ordered α] [topological_space α] [order_topology α]
{δ : Type*} [linear_order δ] [topological_space δ]
[order_closed_topology δ] {a b : α} {f : α → δ} (hf : continuous_on f (interval a b)) :
interval (f a) (f b) ⊆ f '' interval a b := sorry
example : (interval (exp 0) (exp 1)) ⊆ exp '' (interval 0 1) :=
@intermediate_value_interval ℝ _ _ _ _ ℝ _ _ _ 0 1 exp continuous_exp.continuous_on
```

Note that it won't happen with `Icc`

s, because the def of `Icc`

only requires a `preorder`

, and the `preorder`

instances are indeed defeq.

Is there any way around this issue that doesn't require a ton of refactoring ?

#### Yury G. Kudryashov (Feb 13 2021 at 19:31):

Could you please try to remove `decidable_le`

from the definition of src#real.conditionally_complete_linear_order?

#### Yury G. Kudryashov (Feb 13 2021 at 19:32):

It is now included into docs#linear_order

#### Anatole Dedecker (Feb 13 2021 at 19:38):

I'll try this, thanks !

#### Anatole Dedecker (Feb 13 2021 at 20:19):

It works !

#### Anatole Dedecker (Feb 13 2021 at 20:24):

Last updated: May 18 2021 at 06:15 UTC