Mathlib v3 is deprecated. Go to Mathlib v4

Def joined.extend

Modification history

2020-07-30 01:14

src/topology/path_connected.lean

Revert "feat(topology): path connected spaces" …

Deleted joined.extend View on Github →

2020-07-30 01:12

src/topology/path_connected.lean

feat(topology): path connected spaces

Added joined.extend View on Github →