Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-12 11:23 2cbeed95

View on Github →

style(*): use notation 𝓝 for nhds (#1582)

  • chore(*): notation for nhds
  • Convert new uses of nhds

Estimated changes

modified theorem fderiv_congr_of_mem_nhds
modified theorem fderiv_within_inter
modified theorem has_fderiv_within_at_inter
modified theorem tangent_cone_inter_nhds
modified theorem unique_diff_within_at.inter
modified theorem unique_diff_within_at_inter
modified theorem real.tendsto_log_one_zero
modified theorem hyperreal.is_st_of_tendsto
modified theorem exists_nhds_split4
modified theorem exists_nhds_split
modified theorem exists_nhds_split_inv
modified theorem nhds_is_mul_hom
modified theorem nhds_one_symm
modified theorem nhds_pointwise_mul
modified theorem nhds_translation
modified def has_sum
modified theorem tendsto_mul'
modified theorem open_subgroup.mem_nhds_one
modified theorem Liminf_eq_of_le_nhds
modified theorem Liminf_nhds
modified theorem Limsup_eq_of_le_nhds
modified theorem Limsup_nhds
modified theorem ge_mem_nhds
modified theorem gt_mem_nhds
modified theorem is_bounded_ge_nhds
modified theorem is_bounded_le_nhds
modified theorem is_cobounded_ge_nhds
modified theorem is_cobounded_le_nhds
modified theorem le_mem_nhds
modified theorem lt_mem_nhds
modified theorem mem_nhds_orderable_dest
modified theorem tendsto_max
modified theorem tendsto_min
modified theorem closure_eq_nhds
modified def continuous_at
modified theorem interior_eq_nhds
modified theorem is_closed_iff_nhds
modified theorem is_open_iff_mem_nhds
modified theorem is_open_iff_nhds
modified theorem le_nhds_iff
modified theorem lim_spec
modified theorem mem_closure_iff_nhds
modified theorem mem_of_nhds
modified theorem nhds_def
modified theorem nhds_le_of_le
modified theorem nhds_neq_bot
modified theorem nhds_sets
modified theorem pure_le_nhds
modified theorem tendsto_const_nhds
modified theorem map_nhds_subtype_val_eq
modified theorem nhds_prod_eq
modified theorem nhds_swap
modified theorem continuous_within_at_inter
modified theorem inter_mem_nhds_within
modified theorem mem_nhds_within_of_mem_nhds
modified def nhds_within
modified theorem nhds_within_restrict'
modified theorem nhds_within_univ
modified theorem dense_inducing.extend_eq
modified theorem complex.tendsto_inv
modified theorem ennreal.Icc_mem_nhds
modified theorem ennreal.coe_range_mem_nhds
modified theorem ennreal.nhds_coe
modified theorem ennreal.nhds_coe_coe
modified theorem ennreal.nhds_of_ne_top
modified theorem ennreal.nhds_top
modified theorem ennreal.nhds_zero
modified theorem ennreal.tendsto_of_real
modified theorem nnreal.tendsto_of_real
modified theorem real.tendsto_inv
modified theorem nhds_list
modified theorem nhds_nil
modified theorem inducing.map_nhds_eq
modified theorem is_open_map_iff_nhds_le
modified theorem metric.ball_mem_nhds
modified theorem metric.mem_nhds_iff
modified theorem metric.nhds_eq
modified theorem nhds_comap_dist
modified theorem emetric.ball_mem_nhds
modified theorem emetric.mem_nhds_iff
modified theorem emetric.nhds_eq
modified theorem map_nhds_induced_eq
modified theorem compl_singleton_mem_nhds
modified theorem eq_of_nhds_neq_bot
modified theorem lim_eq
modified theorem lim_nhds_eq
modified theorem nhds_eq_nhds_iff
modified theorem nhds_is_closed
modified theorem nhds_le_nhds_iff
modified theorem t2_iff_nhds
modified theorem convergent_eqv_pure
modified theorem ultrafilter_comap_pure_nhds
modified def compact
modified theorem nhds_eq_comap_uniformity
modified theorem nhds_eq_uniformity
modified theorem cauchy_nhds
modified def is_complete