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.
