Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-03 17:56 b51f18f7

View on Github →

feat(topology): properties about intervals and paths (#9914)

  • From the sphere eversion project
  • Properties about paths, the interval, and proj_Icc

Estimated changes

added theorem set.proj_Icc_eq_left
added theorem set.proj_Icc_eq_right
added theorem continuous.Icc_extend'
modified theorem continuous.Icc_extend
added theorem continuous.path_extend
modified theorem path.refl_range
modified theorem path.refl_symm
modified theorem path.symm_range
added theorem proj_Icc_eq_one
added theorem proj_Icc_eq_zero
added theorem unit_interval.coe_mul
added theorem unit_interval.le_one'
added theorem unit_interval.mul_mem
added theorem unit_interval.nonneg'