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 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 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 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 nhds_list
modified theorem nhds_nil
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