Theorem homotopic_of_indiscrete

Modification history

2026-05-19 19:46
Mathlib/Topology/Homotopy/Contractible.lean
feat: add `IndiscreteTopology` instances (#38097)
Added homotopic_of_indiscreteView on Github →