## Stream: maths

### Topic: topology induced by a linear order

#### Kevin Buzzard (Mar 14 2019 at 20:04):

@Calle Sönne and I have a linearly ordered ring and want to talk about sequences tending to limits, so we either need the order topology, or the nhds x filter, consisting of sets which contain open intervals as a subset.

#### Kevin Buzzard (Mar 14 2019 at 20:04):

Is this in mathlib?

#### Patrick Massot (Mar 14 2019 at 20:33):

https://github.com/leanprover-community/mathlib/blob/master/src/topology/algebra/ordered.lean

#### Calle Sönne (Mar 14 2019 at 20:43):

We had a look at that but doesnt this assume there already is a topology?

#### Chris Hughes (Mar 14 2019 at 20:49):

There's the orderable topology, I guess.

#### Chris Hughes (Mar 14 2019 at 20:52):

Just make orderable_topology and topological_space variables.

#### Chris Hughes (Mar 14 2019 at 20:53):

orderable_topology says the topology is equal, but not necessarily definitionally equal to the generate_from {s | ∃a, s = {b : α | a < b} ∨ s = {b : α | b < a}}.

#### Kevin Buzzard (Mar 14 2019 at 21:09):

Like this:

variables {α : Type*} [linear_ordered_ring α] [floor_ring α]

instance : topological_space α :=
topological_space.generate_from {s | ∃a, s = {b : α | a < b} ∨ s = {b : α | b < a}}

instance : orderable_topology α := ⟨rfl⟩


?

#### Chris Hughes (Mar 14 2019 at 21:18):

Like this
variables {α : Type*} [linear_ordered_ring α] [floor_ring α] [topological_space α] [orderable_topology α]

Oh penny drops

#### Chris Hughes (Mar 14 2019 at 21:20):

Otherwise your theorems won't apply to the reals.

#### Chris Hughes (Mar 14 2019 at 21:21):

I guess that's probably enough to deduce topological_ring

#### Kevin Buzzard (Mar 14 2019 at 21:21):

don't get us started on topological rings

#### Kevin Buzzard (Mar 14 2019 at 21:22):

Johan and I have been thinking about them all week

Last updated: May 18 2021 at 08:14 UTC