Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-17 16:13 0b350228

View on Github →

refactor: change variables order in some composition lemmas (#1035)

Estimated changes

Modified src/analysis/complex/exponential.lean

Modified src/analysis/complex/polynomial.lean

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/deriv.lean

added theorem has_fderiv_at.comp_has_fderiv_within_at

deleted theorem has_fderiv_within_at.comp_has_fderiv_at

Modified src/category_theory/concrete_category.lean

Modified src/measure_theory/borel_space.lean

Modified src/measure_theory/giry_monad.lean

Modified src/measure_theory/integration.lean

Modified src/measure_theory/measurable_space.lean

Modified src/measure_theory/measure_space.lean

modified theorem measure_theory.measure.map_map

Modified src/topology/algebra/continuous_functions.lean

Modified src/topology/algebra/group.lean

Modified src/topology/algebra/group_completion.lean

Modified src/topology/algebra/monoid.lean

Modified src/topology/algebra/ring.lean

Modified src/topology/algebra/uniform_group.lean

Modified src/topology/algebra/uniform_ring.lean

Modified src/topology/basic.lean

modified theorem continuous.comp

Modified src/topology/bounded_continuous_function.lean

Modified src/topology/compact_open.lean

modified def continuous_map.induced

Modified src/topology/constructions.lean

Modified src/topology/instances/complex.lean

Modified src/topology/instances/ennreal.lean

Modified src/topology/instances/nnreal.lean

Modified src/topology/instances/real.lean

Modified src/topology/maps.lean

modified theorem embedding_compose

Modified src/topology/metric_space/basic.lean

Modified src/topology/metric_space/completion.lean

Modified src/topology/metric_space/gromov_hausdorff.lean

Modified src/topology/metric_space/isometry.lean

modified theorem isometry.comp

Modified src/topology/uniform_space/completion.lean

modified theorem uniform_space.completion.map_comp