Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-20 20:30 1f74ddd2

View on Github →

feat(topology/local_extr): add lemmas on composition with continuous functions (#3459)

Estimated changes

Modified src/topology/local_extr.lean

added theorem is_local_extr_on.comp_continuous_on

added theorem is_local_max_on.comp_continuous_on

added theorem is_local_min_on.comp_continuous_on