Different linear orders on reals

Stream: maths

[Anatole Dedecker]

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]

Could you please try to remove decidable_le from the definition of src#real.conditionally_complete_linear_order?

[Yury G. Kudryashov]

It is now included into docs#linear_order

[Anatole Dedecker]

I'll try this, thanks !

[Anatole Dedecker]

It works !

[Anatole Dedecker]

#6223