Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-14 08:28 a3bb2050

View on Github →

feat(topology/separation): generalize&rename a lemma (#16503)

  • rename tot_sep_of_zero_dim to totally_separated_space_of_t1_of_basis_clopen;
  • generalize it from a t2_space to a t1_space.

Estimated changes

modified theorem eq.subset
deleted theorem tot_sep_of_zero_dim