# Commit 2023-01-30 21:46 bcfa7268

View on Github →refactor(topology/{order,*}): review API (#18312)

## Main changes

- Switch from
`@[class] structure topological_space`

to`class`

. - Introduce notation
`is_open[t]`

/`is_closed[t]`

/`𝓤[u]`

and use it instead of`t.is_open`

/`@is_closed _ t`

/`u.uniformity`

- Don't introduce a temporary order on
`topological_space`

, use`galois_coinsertion`

to the order-dual of`set (set α)`

instead. - Drop
`discrete_topology_bot`

. It seems that this instance doesn't work well in Lean 4 (in fact, I failed to define it without using`@DiscreteTopology.mk`

).

## Other changes

### Topological spaces

- Add
`is_open_mk`

. - Rename
`generate_from_mono`

to`generate_from_anti`

, move it to the`topological_space`

namespace. - Add
`embedding_inclusion`

,`embedding_ulift_down`

, and`ulift.discrete_topology`

. - Move
`discrete_topology.of_subset`

from`topology.separation`

to`topology.constructions`

. - Move
`embedding.discrete_topology`

from`topology.separation`

to`topology.maps`

. - Use explicit arguments in an argument of
`nhds_mk_of_nhds`

. - Move some definitions and lemmas like
`mk_of_closure`

,`gi_generate_from`

(renamed to`gci_generate_from`

),`left_inverse_generate_from`

to the`topological_space`

namespace. These lemmas are very specific and use generic names. - Add
`topological_space`

and`discrete_topology`

instances for`fin n`

. - Drop
`is_open_induced_iff'`

, use non-primed version instead. - Prove
`set_of_is_open_sup`

by`rfl`

. - Drop
`nhds_bot`

, use`nhds_discrete`

instead. - Drop
`induced_bot`

and`discrete_topology_induced`

### Uniform spaces

- Drop
`infi_uniformity'`

and`inf_uniformity'`

. - Use
`@uniformity α (uniform_space.comap _ _)`

instead of`(h : ‹uniform_space α› = uniform_space.comap f ‹uniform_space β›)`

in`uniformity_comap`

.

### Locally constant functions and discrete quotients

- Use quotient space topology for the coercion of a
`discrete_quotient`

to`Type*`

, then prove`[discrete_topology]`

. This way we avoid surprising diamonds in the future (especially if Lean 4 will unfold the coercion). - Merge
`locally_constant.lift`

and`locally_constant.locally_constant_lift`

into 1 def, rename`factors`

to`lift_comp_proj`

. - Protect
`locally_constant.is_locally_constant`

. - Drop
`locally_constant.iff_continuous_bot`

### Categories

- Add an instance for
`discrete_topology (discrete.obj X)`

. - Rename
`Fintype.discrete_topology`

to`Fintype.bot_topology`

, add lemma`Fintype.discrete_topology`

sating that this is a`[discrete_topology]`

.

### Topological rings

- Fix&golf a proof that failed because of API changes.