Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-13 00:00 ede73b25

View on Github →

refactor(topology/separation): rename regular_space to t3_space (#15169) I'm going to add a version of regular_space without t0_space and prove, e.g., that any uniform space is a regular space in this sense. To do this, I need to rename the existing regular_space.

Estimated changes

modified theorem nhds_basis_closed_balanced
modified theorem has_sum.prod_fiberwise
modified theorem has_sum.sigma
modified theorem has_sum.sigma_of_has_sum
modified theorem summable.sigma'
modified theorem tsum_comm'
modified theorem tsum_prod'
modified theorem tsum_sigma'
modified theorem continuous_extend_from
modified theorem continuous_on_extend_from
modified theorem closed_nhds_basis
modified theorem disjoint_nested_nhds
modified theorem exists_compact_between
modified theorem nhds_is_closed