Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-10 18:16 4a013fb0

View on Github →

feat(analysis): sequential completeness

Estimated changes

Modified analysis/metric_space.lean

added theorem cauchy_seq_metric'

added theorem cauchy_seq_metric

added theorem continuous_topo_metric

modified theorem exists_delta_of_continuous

added theorem tendsto_at_top_metric

added theorem tendsto_nhds_topo_metric

Modified analysis/topology/uniform_space.lean

added def cauchy_seq

added theorem cauchy_seq_tendsto_of_complete

Modified data/real/cau_seq_filter.lean

deleted theorem cau_filter_lim_spec

added theorem cau_seq_iff_cauchy_seq

deleted theorem cau_seq_of_cau_filter_mem_set_seq

modified theorem cauchy_of_filter_cauchy

added theorem complete_of_cauchy_seq_tendsto

modified theorem filter_cauchy_of_cauchy

deleted theorem is_cau_seq_of_dist_tendsto_0

deleted theorem le_nhds_cau_filter_lim

deleted theorem mono_of_mono_succ

deleted theorem seq_of_cau_filter_is_cauchy'

deleted theorem seq_of_cau_filter_is_cauchy

deleted theorem seq_of_cau_filter_mem_set_seq

added theorem sequentially_complete.cauchy_seq_of_dist_tendsto_0

added theorem sequentially_complete.le_nhds_cau_filter_lim

added theorem sequentially_complete.mono_of_mono_succ

added theorem sequentially_complete.seq_of_cau_filter_is_cauchy'

added theorem sequentially_complete.seq_of_cau_filter_is_cauchy

added theorem sequentially_complete.seq_of_cau_filter_mem_set_seq

added def sequentially_complete.set_seq_of_cau_filter

added theorem sequentially_complete.set_seq_of_cau_filter_inhabited

added theorem sequentially_complete.set_seq_of_cau_filter_mem_sets

added theorem sequentially_complete.set_seq_of_cau_filter_monotone'

added theorem sequentially_complete.set_seq_of_cau_filter_monotone

added theorem sequentially_complete.set_seq_of_cau_filter_spec

added theorem sequentially_complete.tendsto_div

deleted def set_seq_of_cau_filter

deleted theorem set_seq_of_cau_filter_inhabited

deleted theorem set_seq_of_cau_filter_mem_sets

deleted theorem set_seq_of_cau_filter_monotone'

deleted theorem set_seq_of_cau_filter_monotone

deleted theorem set_seq_of_cau_filter_spec

deleted theorem tendsto_div

modified theorem tendsto_limit