Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-11 03:45 476f28f8

View on Github →

feat(analysis/analytic/uniqueness): two analytic functions that coincide locally coincide globally (#16723) Higher dimensional version of #16489.

Estimated changes

Modified src/analysis/analytic/isolated_zeros.lean

deleted theorem analytic_on.eq_on_of_preconnected_of_frequently_eq'

modified theorem analytic_on.eq_on_of_preconnected_of_frequently_eq

deleted theorem analytic_on.eq_on_of_preconnected_of_mem_closure'

modified theorem analytic_on.eq_on_of_preconnected_of_mem_closure

added theorem analytic_on.eq_on_zero_of_preconnected_of_frequently_eq_zero

added theorem analytic_on.eq_on_zero_of_preconnected_of_mem_closure

Created src/analysis/analytic/uniqueness.lean

added theorem analytic_on.eq_on_of_preconnected_of_eventually_eq

added theorem analytic_on.eq_on_zero_of_preconnected_of_eventually_eq_zero

added theorem analytic_on.eq_on_zero_of_preconnected_of_eventually_eq_zero_aux

Modified src/topology/connected.lean

added theorem is_preconnected.subset_of_closure_inter_subset