Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-14 16:39 f443792f

View on Github →

feat(topology/subset_properties): add instances for totally_disconnected_spaces (#5334) Add the instances subtype.totally_disconnected_space and pi.totally_disconnected_space.

Estimated changes