Commit 2023-11-03 09:34 0bc95f40

View on Github →

feat: add totallyDisconnectedSpace_subtype_iff (#8134) Also add a version about Embedding. Motivated by a lemma in the Mandelbrot Set Connectedness Project.

Estimated changes

Modified Mathlib/Topology/Connected/TotallyDisconnected.lean

added theorem Embedding.isTotallyDisconnected_image

added theorem Embedding.isTotallyDisconnected_range

added theorem totallyDisconnectedSpace_subtype_iff