Theorem isPathConnected_compl_of_isPathConnected_compl_zero

Modification history

2025-05-12 15:03
Mathlib/Analysis/Convex/PathConnected.lean
feat: define `Path.segment` (#24761) …
Modified isPathConnected_compl_of_isPathConnected_compl_zeroView on Github →
2025-05-11 18:08
Mathlib/Analysis/Convex/Topology.lean
chore(Convex/Topology): golf (#24765) …
Modified isPathConnected_compl_of_isPathConnected_compl_zeroView on Github →
2024-04-17 13:43
Mathlib/Analysis/Convex/Topology.lean
feat: codimension two subspaces have path-connected complement (#11337) …
Added isPathConnected_compl_of_isPathConnected_compl_zeroView on Github →