Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-15 18:05 7130d75d

View on Github โ†’

chore(*): introduce notation for left/right/punctured nhds (#10694) New notation:

  • ๐“[โ‰ค] x: the filter nhds_within x (set.Iic x) of left-neighborhoods of x;
  • ๐“[โ‰ฅ] x: the filter nhds_within x (set.Ici x) of right-neighborhoods of x;
  • ๐“[<] x: the filter nhds_within x (set.Iio x) of punctured left-neighborhoods of x;
  • ๐“[>] x: the filter nhds_within x (set.Ioi x) of punctured right-neighborhoods of x;
  • ๐“[โ‰ ] x: the filter nhds_within x {x}แถœ of punctured neighborhoods of x.

Estimated changes

modified theorem real.map_exp_at_bot
modified theorem real.tendsto_cos_pi_div_two
modified theorem real.tendsto_sin_pi_div_two
modified theorem real.tendsto_tan_pi_div_two
modified theorem tendsto_inv_at_top_zero'
modified theorem tendsto_inv_zero_at_top
modified theorem closure_compl_singleton
modified theorem dense_compl_singleton
modified theorem interior_singleton
modified theorem dense.diff_finite
modified theorem dense.diff_finset
modified theorem dense.diff_singleton
modified theorem infinite_of_mem_nhds