Commit 2020-03-04 19:56 9fc675c4
View on Github →chore(analysis/normed_space/basic): rename ne_mem_of_tendsto_norm_at_top (#2085)
It uses ∀ᶠ now, so rename to eventually_ne_of_tendsto_norm_at_top.
chore(analysis/normed_space/basic): rename ne_mem_of_tendsto_norm_at_top (#2085)
It uses ∀ᶠ now, so rename to eventually_ne_of_tendsto_norm_at_top.