Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-09 17:36 bf25d26f

View on Github →

chore(data/set/intervals/proj_Icc): add strict_mono_incr_on (#5292)

  • rename set.Icc_extend_monotone to monotone.Icc_extend;
  • add set.strict_mono_incr_on_proj_Icc and strict_mono.strict_mono_incr_on_Icc_extend.

Estimated changes

added theorem monotone.Icc_extend
deleted theorem set.Icc_extend_monotone