Open Ioi

Stream: mathlib4

[Yury G. Kudryashov]

We have docs#isOpen_Ioi and docs#isOpen_lt' with different assumptions:

• isOpen_Ioi assumes [LinearOrder α] [OrderClosedTopology α]
• isOpen_lt' assumes [Preorder α] [OrderTopology α]

then we have lemmas randomly choosing between these two assumptions, sometimes duplicating API. How should we deal with this?

[Yury G. Kudryashov]

/poll What should we do with isOpen_Ioi etc?
add typeclasses OpenIoiTopology and OpenIioTopology with instances for LinearOrder+ClosedI**Topology and OrderTopology
decide that we don't care about OrderTopology unless it's a LinearOrder, migrate to ClosedI**Topology everywhere

[Yaël Dillies]

Ioi (0 : Real x Real) is not open, which I take as a strong argument towards the second option

[Yury G. Kudryashov]

I don't know if it's possible to describe the topology in terms of a preorder so that it gives the correct answer for (indexed) products of linear orders.

[Yury G. Kudryashov]

I have an answer in case of finite products:

• introduce a distance between points so that x and y are at distance 1 if x ≤ y and Icc x y is a chain;
• let n be the maximal distance between points;
• for each x, the set of points y such that x < y and they're at distance n is open, same with reversed roles;
• the topology is generated by sets like :up: this

[Yury G. Kudryashov]

@Yaël Dillies related question: am I right that a SuccOrder is a disjoint union of linear orders? Is there a reason to care about non linearly ordered SuccOrders?

[Yaël Dillies]

No, that's incorrect. SuccOrder only tells you local information. As soon as there are infinitely many elements between x and y, SuccOrder doesn't tell you anything about how they're related.

[Yaël Dillies]

Eg take N x_lex (N x N)

[Yaël Dillies]

This is a bunch of copies of N (hence a SuccOrder) ordered non-linearly (hence not a disjoint union of linear orders)

[Yury G. Kudryashov]

So, it makes sense to prove, e.g., [Preorder α] [SuccOrder α] [PredOrder α] : DiscreteTopology α without LinearOrder α assumption. Then we're back to my original question.

[Yaël Dillies]

I'm not claiming we care about those examples in practice, however. They just happen to naturally fit my definition.

[Yaël Dillies]

Yeah no, I wouldn't worry too much about trying to include those examples

[Yury G. Kudryashov]

Then I'm going to rewrite Topology/Order/Basic so that we assume ClosedIxxTopology for lemmas like this.

[Yury G. Kudryashov]

(and probably split it into OrderClosedTopology and OrderTopology)

[Yaël Dillies]

Yeah that makes sense. Btw I think we need to signal more clearly what typeclasses are of the form "Your topology is exactly blah" vs "Your topology has property blah".

[Yury G. Kudryashov]

I suggest that "move things around" and "rename typeclasses" are different PRs.

[Yaël Dillies]

Yes of course, although I was more thinking of rewriting the typeclasses docstrings rather than renaming them in my previous message

[Yury G. Kudryashov]

That's even easier. I didn't check the docstrings for a while.

[Aaron Liu]

Yury G. Kudryashov said:

I don't know if it's possible to describe the topology in terms of a preorder so that it gives the correct answer for (indexed) products of linear orders.

Closed sets generated by closed intervals seems to work

[Yury G. Kudryashov]

Can you prove this?

def myTopology (X : Type*) [PartialOrder X] : TopologicalSpace X := sorry -- your def

theorem myTopology_eq {ι : Type*} [Finite ι] (X : ι → Type*) [∀ i, LinearOrder (X i)] [∀ i, TopologicalSpace (X i)]
    [∀ i, OrderTopology (X i)] : myTopology (∀ i, X i) = inferInstance := _

[Aaron Liu]

The previous idea doesn't work, but I have a new idea I'll try proving that with (I think it generates the box topology :()

[Yury G. Kudryashov]

OTOH, you can try to construct two finite products of linear orders with OrderTopology and a discontinuous OrderIso between them.