Mathlib Changelog
v3
Changelog
About
Github
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