## Stream: general

### Topic: how to work with order topologies?

#### Eric Rodriguez (Nov 27 2021 at 22:58):

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,
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 (Nov 27 2021 at 23:01):

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

#### Yaël Dillies (Nov 27 2021 at 23:02):

You might need #3292 to do what you want.

#### Reid Barton (Nov 27 2021 at 23:03):

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

#### Eric Rodriguez (Nov 27 2021 at 23:03):

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

#### Reid Barton (Nov 27 2021 at 23:03):

Generalize to what though?

#### Eric Rodriguez (Nov 27 2021 at 23:04):

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

#### Heather Macbeth (Nov 27 2021 at 23:40):

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 (Nov 27 2021 at 23:45):

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 (Nov 28 2021 at 01:33):

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

Last updated: Dec 20 2023 at 11:08 UTC