Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-26 11:40 bfc05842

View on Github →

refactor(topology,analysis): use maps_to in lemmas like continuous_on.comp (#12294)

Estimated changes

Modified src/analysis/calculus/fderiv.lean

Modified src/analysis/normed_space/basic.lean

Modified src/data/set/function.lean

modified theorem set.maps_to.mono

added theorem set.maps_to.mono_left

added theorem set.maps_to.mono_right

Modified src/dynamics/omega_limit.lean

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

added theorem model_with_corners.continuous_on_symm

Modified src/measure_theory/integral/divergence_theorem.lean

Modified src/measure_theory/integral/interval_integral.lean

Modified src/topology/continuous_on.lean

Modified src/topology/fiber_bundle.lean