Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-14 20:35 5c19b83b

View on Github →

feat(analysis/complex/open_mapping): the open mapping thm for holomorphic functions (#16780)

Estimated changes

Modified src/analysis/analytic/basic.lean

added theorem analytic_on.mono

Modified src/analysis/analytic/isolated_zeros.lean

added theorem analytic_at.eventually_eq_or_eventually_ne

added theorem analytic_at.frequently_eq_iff_eventually_eq

Modified src/analysis/calculus/deriv.lean

modified theorem differentiable.inv

modified theorem differentiable_at.inv

modified theorem differentiable_on.inv

modified theorem differentiable_within_at.inv

Modified src/analysis/complex/abs_max.lean

added theorem complex.eventually_eq_or_eq_zero_of_is_local_min_norm

Modified src/analysis/complex/cauchy_integral.lean

added theorem differentiable_on.analytic_on

Created src/analysis/complex/open_mapping.lean

added theorem analytic_at.eventually_constant_or_nhds_le_map_nhds

added theorem analytic_at.eventually_constant_or_nhds_le_map_nhds_aux

added theorem analytic_on.is_constant_or_is_open

added theorem diff_cont_on_cl.ball_subset_image_closed_ball

Modified src/analysis/normed/group/basic.lean

added theorem norm_div_sub_norm_div_le_norm_div

Modified src/topology/algebra/field.lean

added theorem is_local_min.inv

Modified src/topology/algebra/order/compact.lean

added theorem is_compact.exists_local_min_mem_open

added theorem is_compact.exists_local_min_on_mem_subset

Modified src/topology/metric_space/basic.lean

added theorem metric.exists_local_min_mem_ball