Zulip Chat Archive

Stream: maths

Topic: Different linear orders on reals


view this post on Zulip 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 ?

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Feb 13 2021 at 19:32):

It is now included into docs#linear_order

view this post on Zulip Anatole Dedecker (Feb 13 2021 at 19:38):

I'll try this, thanks !

view this post on Zulip Anatole Dedecker (Feb 13 2021 at 20:19):

It works !

view this post on Zulip Anatole Dedecker (Feb 13 2021 at 20:24):

#6223


Last updated: May 18 2021 at 06:15 UTC