## 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 Iccs, 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 !

It works !

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

#6223

Last updated: May 18 2021 at 06:15 UTC