Commit 2026-05-19 19:46 1e3f5a3c

View on Github →

feat: add IndiscreteTopology instances (#38097)

Estimated changes

Modified Mathlib/Topology/Homotopy/Contractible.lean

added theorem homotopic_of_indiscrete

added theorem nullhomotopic_of_indiscrete

Modified Mathlib/Topology/Inseparable.lean

Modified Mathlib/Topology/NoetherianSpace.lean

Modified Mathlib/Topology/Separation/Connected.lean

added theorem subsingleton_iff_discrete_and_indiscrete