Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-14 10:07 61054f70

View on Github →

feat(topology): some improvements (#11424)

  • Prove a better version of continuous_on.comp_fract. Rename continuous_on.comp_fract -> continuous_on.comp_fract''.
  • Rename finset.closure_Union -> finset.closure_bUnion
  • Add continuous.congr and continuous.subtype_coe

Estimated changes

modified theorem continuous_on.comp_fract'
modified theorem continuous_on.comp_fract
added theorem continuous.congr
deleted theorem finset.closure_Union
added theorem finset.closure_bUnion
added theorem continuous.subtype_coe