Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-05 09:09 545186ca

View on Github →

refactor(*): add a notation for nhds_within (#3683) The definition is still there and can be used too.

Estimated changes

modified theorem has_deriv_within_at_inter'
modified theorem has_fderiv_within_at_inter'
modified theorem tangent_cone_congr
modified theorem tangent_cone_mono_nhds
modified theorem unique_diff_within_at_congr
modified theorem continuous_within_at_inter'
modified theorem mem_nhds_within_insert
modified theorem mem_nhds_within_subtype
modified theorem mem_of_mem_nhds_within
modified theorem nhds_within_empty
modified theorem nhds_within_le_of_mem
modified theorem nhds_within_mono
modified theorem nhds_within_restrict''
modified theorem nhds_within_univ
modified theorem self_mem_nhds_within
modified def is_local_extr_on
modified def is_local_max_on
modified def is_local_min_on
modified theorem metric.mem_nhds_within_iff