Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-06 10:58 9615b385

View on Github →

feat(data/real): completeness criterion for Cauchy sequences (closes #654)

Estimated changes

Modified src/data/real/cau_seq_filter.lean

modified theorem complete_of_cauchy_seq_tendsto

added theorem emetric.complete_of_convergent_controlled_sequences

added theorem metric.complete_of_convergent_controlled_sequences

added theorem sequentially_complete.FB_lim

added theorem sequentially_complete.FB_pos

added theorem sequentially_complete.F_lim

added theorem sequentially_complete.F_pos

deleted theorem sequentially_complete.cauchy_seq_of_dist_tendsto_0

modified theorem sequentially_complete.le_nhds_cau_filter_lim

added theorem sequentially_complete.seq_of_cau_filter_bound

deleted theorem sequentially_complete.seq_of_cau_filter_is_cauchy'

modified theorem sequentially_complete.seq_of_cau_filter_mem_set_seq

modified theorem sequentially_complete.set_seq_of_cau_filter_inhabited

modified theorem sequentially_complete.set_seq_of_cau_filter_mem_sets