order and topology

Stream: maths

[Yury G. Kudryashov]

We have docs#order_topology and docs#order_closed_topology. In case of a partial order (e.g., a product of two linear orders), none of the typeclasses implies the other (and we only have order_closed_topology (α × α) for the product topology). So, we have docs#is_open_Ioi and docs#is_open_lt' with different typeclass assumptions. At the same time, there are many properties that are true for an (indexed or not) product of linear orders with order topology. I've recently introduced a few classes like docs#compact_Icc_space to have theorems stated uniformly for all these cases.

So, I have two questions:

1. Are there natural instances for [order_topology α] when α is not a linear order?
2. Does anyone know a nice set of axioms that works for (indexed) products of linear orders and implies, e.g., docs#is_compact_Icc and docs#tendsto_at_top_supr?

[Johan Commelin]

cc @Yaël Dillies :wink:

[Yaël Dillies]

Ahah! I was actually about this no later than yesterday. Haven't come to a conclusion yet.

[Yury G. Kudryashov]

It seems that I know a typeclass that works for (finite, indexed) products of linear orders (not tested). I don't know whether we can prove many theorems based on this typeclass.

variables {α : Type*} [preorder α]

def strong_lt (a b : α) : Prop :=
a < b ∧ ∀ c < b, ∃ d < b, a ≤ d ∧ c ≤ d

def IiO (a : α) := {b | strong_lt b a}
def IOi (a : α) := {b | strong_lt a b}

variable (α)

def preorder_topology' : topological_space α :=
topological_space.generate_from (range IiO ∪ range IOi)

class order_topology' [t : topological_space α] : Prop := (out : t = preorder_topology' α)

[Yury G. Kudryashov]

There are quite a few issues with this definition. E.g., it seems that @strong_lt (order_dual α) _ a b ≠ strong_lt b a.

[Yury G. Kudryashov]

What I like about strong_lt is that lemmas like docs#is_lub.exists_between work with this it.