Zulip Chat Archive

Stream: maths

Topic: topology generated by an order


view this post on Zulip 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}\{x : a<x<b\} for each pair (a,b)(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.

view this post on Zulip Mario Carneiro (Aug 15 2018 at 13:08):

note the difference between ordered_topology and orderable_topology

view this post on Zulip Mario Carneiro (Aug 15 2018 at 13:08):

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

view this post on Zulip Mario Carneiro (Aug 15 2018 at 13:09):

the former is more like an order-respecting topology

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 15 2018 at 13:57):

Aah this is perfect -- orderable_topology is exactly what we want. Thanks!

view this post on Zulip 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.leanand 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?

view this post on Zulip Mario Carneiro (Aug 16 2018 at 10:48):

this should be an easy consequence of frontier_le_subset_eq

view this post on Zulip 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}

view this post on Zulip Mario Carneiro (Aug 16 2018 at 10:59):

added

view this post on Zulip 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! :)

view this post on Zulip 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