topology generated by an order

Stream: maths

[Kevin Buzzard]

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]

note the difference between ordered_topology and orderable_topology

[Mario Carneiro]

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

[Mario Carneiro]

the former is more like an order-respecting topology

[Mario Carneiro]

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]

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]

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

[Luca Gerolla]

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?

[Mario Carneiro]

this should be an easy consequence of frontier_le_subset_eq

[Mario Carneiro]

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]

added

[Luca Gerolla]

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]

Also nice addition frontier_compl! ..I had better update my mathlib