Theorem IsPathConnected.exists_path_through_family'

Modification history

2023-10-26 13:37

Mathlib/Topology/Connected/PathConnected.lean

feat: path-connectedness is preserved by homeomorphisms (#7878) …

Modified IsPathConnected.exists_path_through_family'View on Github →

2023-08-10 19:52

Mathlib/Topology/PathConnected.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified IsPathConnected.exists_path_through_family'View on Github →

2023-03-23 16:06

Mathlib/Topology/PathConnected.lean

feat: port Topology.PathConnected (#2755) …

Added IsPathConnected.exists_path_through_family'View on Github →