Zulip Chat Archive

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,
                                ..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 (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: Aug 03 2023 at 10:10 UTC