Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-20 21:53 d774ef68

View on Github →

feat(topology/path_connected): add lemmas about paths and continuous families of paths (#4063) From the sphere eversion project (see https://github.com/leanprover-community/sphere-eversion/pull/12)

Estimated changes

Modified src/topology/path_connected.lean

added theorem is_path_connected.exists_path_through_family'

added theorem is_path_connected.exists_path_through_family

added theorem path.continuous_uncurry_extend_of_continuous_family

added theorem path.extend_extends'

added theorem path.extend_extends

added theorem path.extend_le_zero

added theorem path.extend_one_le

added theorem path.extend_range

added theorem path.refl_extend

added theorem path.refl_range

added theorem path.refl_symm

added theorem path.refl_trans_refl

added theorem path.symm_cast

added theorem path.symm_continuous_family

added theorem path.symm_range

added theorem path.trans_cast

added theorem path.trans_continuous_family

added theorem path.trans_range

added def path.truncate

added theorem path.truncate_const_continuous_family

added theorem path.truncate_continuous_family

added def path.truncate_of_le

added theorem path.truncate_one_one

added theorem path.truncate_range

added theorem path.truncate_self

added theorem path.truncate_zero_one

added theorem path.truncate_zero_zero

added theorem path_connected_space.exists_path_through_family'

added theorem path_connected_space.exists_path_through_family

added theorem proj_I_one

added theorem proj_I_zero