[Merged by Bors] - refactor(topology/{order,*}): review API

[urkud]

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.

---

[rwbarton]

Use @is_open _ t instead of t.is_open everywhere.

What's the motivation for this? Was something broken that we never noticed? Or is something different in Lean 4?

[urkud]

Use @is_open _ t instead of t.is_open everywhere.

What's the motivation for this? Was something broken that we never noticed? Or is something different in Lean 4?

IMHO, it makes sense to have 1 normal form. Before this change, we had to rw or change from one form to another here and there.

[rwbarton]

I think though that writing t.is_open s is so much more natural than @is_open _ t s that people will write it anyways even if the other one is the normal form.

[urkud]

We can introduce notation like we do for measurable_set (e.g., is_open[t] s). And/or we can add a linter. Unfortunately, we can't make t.is_open the normal form (e.g., with export topological_space (is_open) because then dot notation won't work.

[rwbarton]

If nothing else, let's add a prime to the structure field name then so people don't use it by accident.

[rwbarton]

I think dot notation would still work with the export if we move is_open.* to topological_space.is_open.*, right?

[urkud]

I think dot notation would still work with the export if we move is_open.* to topological_space.is_open.*, right?

Yes but this looks strange.

[jcommelin]

bors d+

[bors]

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[urkud]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests