# Zulip Chat Archive

## 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 α]`

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

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