how to work with order topologies?

Stream: general

[Eric Rodriguez]

So, for example, consider this:

import topology.algebra.polynomial

--example {K} [linear_ordered_field K] : false :=
example {K} [linear_ordered_field K] [conditionally_complete_linear_order K] : false :=
begin
  letI := preorder.topology K,
  letI : order_topology K := ⟨rfl⟩,
  letI : topological_ring K := {..linear_ordered_field.has_continuous_mul,
                                ..linear_ordered_add_comm_group.topological_add_group},
  have := intermediate_value_interval (@polynomial.X K _).continuous_on,
end

Firstly, it's kind of weird that preorder.topology doesn't have an instance of order_topology, but I guess that is a performance consideration or not that important. However, the bigger issue is that neither of these headers work for different reasons; I need the conditionally_complete_linear_order for intermediate_value_interval, but if I add it in (even as a letI) it seems to ruin the topology (even though I'm setting my own!) and making my topological ring declaration fail. I have a feeling I'm using the wrong typeclasses and they're not meant to be mix-ins — what to do here?

[Yaël Dillies]

This looks fishy. Both [linear_ordered_field K] and [conditionally_complete_linear_order K] carry an order on K.

[Yaël Dillies]

You might need #3292 to do what you want.

[Reid Barton]

I was going to say, I guess you have some specialized reason not to just use real?

[Eric Rodriguez]

I was trying to generalize a theorem from ℝ and decided not to use my brain too much :)

[Reid Barton]

Generalize to what though?

[Eric Rodriguez]

Exactly, I'm saying now that you guys point it out I'm basically generalizing from ℝ to "ℝ with extra steps"

[Heather Macbeth]

Eric Rodriguez said:

Firstly, it's kind of weird that preorder.topology doesn't have an instance of order_topology, but I guess that is a performance consideration or not that important.

preorder.topology is a def, not an instance.

[Eric Rodriguez]

yes, but an instance that's meant to be letI'd; in that file I see a lot of letI := preorder.topology α; letI : order_topology α := \<rfl>

[Yury G. Kudryashov]

Lean 3 looks for instances right to left, so it will try to pick this instance every time.