Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-11 07:59 aae8d563

View on Github →

refactor(topology/sequences): golf, review API (#17454)

  • drop lebesgue_number_lemma_seq: use lebesgue_number_lemma + is_seq_compact.is_compact instead;
  • add is_seq_compact.exists_tendsto_of_frequently_mem, is_seq_compact.exists_tendsto, is_seq_compact.is_complete;
  • golf some proofs.

Estimated changes

deleted theorem is_compact.is_seq_compact
deleted theorem lebesgue_number_lemma_seq