Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-23 09:39 3e77124c

View on Github →

refactor(topology/{separation,subset_properties}): use set.subsingleton (#12232) Use set.subsingleton s instead of _root_.subsingleton s in is_preirreducible_iff_subsingleton and is_preirreducible_of_subsingleton, rename the latter to set.subsingleton.is_preirreducible.

Estimated changes