Commit 2024-01-08 11:01 f5eb4a83

View on Github →

chore(Filter/AtTopBot): golf (#9521) Golf lemmas about sequential convergence and related concepts. Also add Filter.frequently_iff_seq_forall.

Estimated changes

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.frequently_iff_seq_forall

deleted theorem Filter.not_tendsto_iff_exists_frequently_nmem

deleted theorem Filter.tendsto_iff_forall_eventually_mem

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.Tendsto.eventually_mem

added theorem Filter.not_tendsto_iff_exists_frequently_nmem

added theorem Filter.tendsto_iff_forall_eventually_mem