Mathlib v3 is deprecated. Go to Mathlib v4

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

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


  • 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.

Estimated changes

modified def is_open
modified theorem is_open_fold
added theorem is_open_mk
modified theorem is_open_univ
deleted structure topological_space
modified theorem topological_space_eq
deleted theorem inf_uniformity'
modified theorem inf_uniformity
deleted theorem infi_uniformity'
modified theorem infi_uniformity
modified theorem uniform_space_comap_id
modified theorem uniform_space_eq
modified theorem uniformity_comap