Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_local_max_on.norm_add_self

Modification history

2022-07-17 04:14
src/analysis/normed_space/extr.lean
feat(analysis/complex/abs_max): add a version of the maximum modulus principle (#15364) …
Added is_local_max_on.norm_add_selfView on Github →