Commit 2025-05-11 18:08 9a5744dd
View on Github →chore(Convex/Topology): golf (#24765)
This PR golfs the proof
of isPathConnected_compl_of_isPathConnected_compl_zero by introducing IsPathConnected.add and dependencies.
Also use ∀ ⦃y⦄ instead of ∀ {y} in the definition of IsPathConnected.