Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-09 11:36 7cb0a851

View on Github →

refactor(topology): rename lim to Lim (#2977) Also introduce lim (f : filter α) (g : α → β).

Estimated changes

added theorem Lim_spec
modified theorem lim_spec
modified theorem dense_inducing.extend_eq
added theorem Lim_eq
added theorem Lim_nhds
added theorem Lim_nhds_within
added theorem continuous.lim_eq
added theorem filter.tendsto.lim_eq
deleted theorem lim_eq
deleted theorem lim_nhds_eq
deleted theorem lim_nhds_eq_of_closure
added theorem lim_nhds_id
added theorem lim_nhds_within_id
added theorem cauchy.le_nhds_Lim
added theorem cauchy_seq.tendsto_lim
deleted theorem le_nhds_lim_of_cauchy