Commit 2025-02-09 22:27 15986855

View on Github →

chore(Topology/Connected): split PathConnected.lean (#21591) Splits Mathlib.Topology.Connected.PathConnected into three files:

  • Mathlib.Topology.Path, which now contains the basic API for paths,
  • Mathlib.Topology.Connected.PathConnected, which retains the work on path components and path-connected sets and spaces,
  • Mathlib.Topology.Connected.LocPathConnected, which now contains everything relating to locally path-connected spaces. While splitting this file I have also taken the liberty to insert my name into the authors list of Mathlib.Topology.Connected.LocPathConnected, as about half the contents of that file are from an earlier PR of mine.

Estimated changes

deleted theorem Continuous.path_eval
deleted theorem Continuous.path_extend
deleted theorem Continuous.path_trans
deleted theorem ContinuousAt.path_extend
deleted def Path.cast
deleted theorem Path.cast_coe
deleted theorem Path.coe_mk
deleted theorem Path.coe_mk_mk
deleted theorem Path.coe_reparam
deleted theorem Path.coe_toContinuousMap
deleted theorem Path.continuous_extend
deleted theorem Path.continuous_symm
deleted theorem Path.continuous_trans
deleted def Path.extend
deleted theorem Path.extend_extends'
deleted theorem Path.extend_extends
deleted theorem Path.extend_of_le_zero
deleted theorem Path.extend_of_one_le
deleted theorem Path.extend_one
deleted theorem Path.extend_range
deleted theorem Path.extend_zero
deleted def Path.map'
deleted def Path.map
deleted theorem Path.map_coe
deleted theorem Path.map_id
deleted theorem Path.map_map
deleted theorem Path.map_symm
deleted theorem Path.map_trans
deleted def Path.ofLine
deleted theorem Path.ofLine_mem
deleted theorem Path.pi_coe
deleted theorem Path.prod_coe
deleted theorem Path.range_reparam
deleted def Path.refl
deleted theorem Path.refl_extend
deleted theorem Path.refl_range
deleted theorem Path.refl_reparam
deleted theorem Path.refl_symm
deleted theorem Path.refl_trans_refl
deleted def Path.reparam
deleted theorem Path.reparam_id
deleted def Path.simps.apply
deleted def Path.symm
deleted theorem Path.symm_bijective
deleted theorem Path.symm_cast
deleted theorem Path.symm_range
deleted theorem Path.symm_symm
deleted def Path.trans
deleted theorem Path.trans_apply
deleted theorem Path.trans_cast
deleted theorem Path.trans_pi_eq_pi_trans
deleted theorem Path.trans_range
deleted theorem Path.trans_symm
deleted def Path.truncate
deleted def Path.truncateOfLE
deleted theorem Path.truncate_one_one
deleted theorem Path.truncate_range
deleted theorem Path.truncate_self
deleted theorem Path.truncate_zero_one
deleted theorem Path.truncate_zero_zero
deleted structure Path
deleted theorem pathComponentIn_mem_nhds
added theorem Continuous.path_eval
added theorem Continuous.path_extend
added theorem Continuous.path_trans
added def Path.cast
added theorem Path.cast_coe
added theorem Path.coe_mk
added theorem Path.coe_mk_mk
added theorem Path.coe_reparam
added theorem Path.continuous_extend
added theorem Path.continuous_symm
added theorem Path.continuous_trans
added def Path.extend
added theorem Path.extend_extends'
added theorem Path.extend_extends
added theorem Path.extend_of_le_zero
added theorem Path.extend_of_one_le
added theorem Path.extend_one
added theorem Path.extend_range
added theorem Path.extend_zero
added def Path.map'
added def Path.map
added theorem Path.map_coe
added theorem Path.map_id
added theorem Path.map_map
added theorem Path.map_symm
added theorem Path.map_trans
added def Path.ofLine
added theorem Path.ofLine_mem
added theorem Path.pi_coe
added theorem Path.prod_coe
added theorem Path.range_reparam
added def Path.refl
added theorem Path.refl_extend
added theorem Path.refl_range
added theorem Path.refl_reparam
added theorem Path.refl_symm
added theorem Path.refl_trans_refl
added def Path.reparam
added theorem Path.reparam_id
added def Path.simps.apply
added def Path.symm
added theorem Path.symm_bijective
added theorem Path.symm_cast
added theorem Path.symm_range
added theorem Path.symm_symm
added def Path.trans
added theorem Path.trans_apply
added theorem Path.trans_cast
added theorem Path.trans_range
added theorem Path.trans_symm
added def Path.truncate
added theorem Path.truncate_one_one
added theorem Path.truncate_range
added theorem Path.truncate_self
added theorem Path.truncate_zero_one
added structure Path