# Zulip Chat Archive

## Stream: maths

### Topic: topology generated by an order

#### Kevin Buzzard (Aug 15 2018 at 12:19):

I don't know in what generality it's meaningful to ask about the topology "generated by" an order. Luca found `ordered_topology`

in `analysis/topology/topological_structures.lean`

but this is an assertion that sets coming from the order are closed in the topology, it doesn't rule out there being far more closed sets.

Here's a concrete question. Is there a theorem in mathlib saying that the topology on the reals is the one associated in some way to the total order `<`

on the reals? Presumably with a total order one can define basic open sets $\{x : a<x<b\}$ for each pair $(a,b)$. Is this all there already and how much further does it go? Seems to work fine for total orders, but probably not for partial orders because we seem to need infs and sups. Is this what a lattice is? I am reluctant to do work that's already there and as you can see I am not currently even sure which files I should be looking in.

#### Mario Carneiro (Aug 15 2018 at 13:08):

note the difference between `ordered_topology`

and `orderable_topology`

#### Mario Carneiro (Aug 15 2018 at 13:08):

the latter is for what topologists usually call "the order topology"

#### Mario Carneiro (Aug 15 2018 at 13:09):

the former is more like an order-respecting topology

#### Mario Carneiro (Aug 15 2018 at 13:10):

Is there a theorem in mathlib saying that the topology on the reals is the one associated in some way to the total order < on the reals?

Yes, this is the instance of `orderable_topology real`

#### Mario Carneiro (Aug 15 2018 at 13:11):

Is this all there already and how much further does it go? Seems to work fine for total orders, but probably not for partial orders because we seem to need infs and sups.

If you look at the definition in `ordered_topology`

, you will see that we require that closed intervals are closed, not that open intervals are open. In partial orders this is more natural. In total orders they are equivalent

#### Kevin Buzzard (Aug 15 2018 at 13:57):

Aah this is perfect -- `orderable_topology`

is exactly what we want. Thanks!

#### Luca Gerolla (Aug 16 2018 at 10:46):

Thank you very much Mario... It was very helpful to understand the different "order_topologies" in `analysis/topology/topological_structures.lean`

and at the end I found the result I needed:

lemma frontier_lt_subset_eq [topological_space α] [decidable_linear_order α] [t : ordered_topology α] [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) : frontier {b | f b < g b} ⊆ {b | f b = g b} := begin unfold frontier, have h₁ : interior {b : β | f b < g b} = {b : β | f b < g b}, exact interior_eq_iff_open.2 (is_open_lt hf hg), rw h₁, have h₂ : closure {b : β | f b < g b} ⊆ closure {b : β | f b ≤ g b}, refine closure_mono _ , rw set.set_of_subset_set_of, intros x h, exact le_of_lt h, have h₃ : closure {b : β | f b ≤ g b} = {b : β | f b ≤ g b}, exact closure_eq_iff_is_closed.2 (is_closed_le hf hg), rw h₃ at h₂ , have g₁ : closure {b : β | f b < g b} \ {b : β | f b < g b} ⊆ {b : β | f b ≤ g b} \ {b : β | f b < g b}, {unfold has_sdiff.sdiff set.diff, intros a Ha, simp at Ha, simp, cases Ha with a₁ a₂ , have h₄ : a ∈ {b : β | f b ≤ g b}, exact set.mem_of_mem_of_subset a₁ h₂, rw mem_set_of_eq at h₄, exact ⟨ h₄, a₂ ⟩ , }, have g₂ : {b : β | f b ≤ g b} \ {b : β | f b < g b} ⊆ {b : β | f b = g b}, unfold has_sdiff.sdiff set.diff, intros a Ha, simp at Ha, rw mem_set_of_eq, exact le_antisymm Ha.1 Ha.2, exact set.subset.trans g₁ g₂, end

By any chance, would this be helpful (with slicker proof) in mathlib in addition to `frontier_le_subset_eq`

?

#### Mario Carneiro (Aug 16 2018 at 10:48):

this should be an easy consequence of `frontier_le_subset_eq`

#### Mario Carneiro (Aug 16 2018 at 10:49):

The frontier of the complement of A is the same as the frontier of A, so each implies the other since `{b | f b < g b}`

is the complement of `{b | g b <= f b} `

#### Mario Carneiro (Aug 16 2018 at 10:59):

added

#### Luca Gerolla (Aug 16 2018 at 11:09):

The frontier of the complement of A is the same as the frontier of A, so each implies the other since

`{b | f b < g b}`

is the complement of`{b | g b <= f b}`

I did try to go along this line of reasoning but I did not find it that shorter ... Definitely not 2 lines like yours! :)

#### Luca Gerolla (Aug 16 2018 at 11:10):

Also nice addition `frontier_compl`

! ..I had better update my mathlib

Last updated: May 14 2021 at 19:21 UTC