Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-02 14:08 e6a1bc35

View on Github →

feat(data/real/cau_seq): relate cauchy sequence completeness and filter completeness

Estimated changes

Modified algebra/archimedean.lean

added theorem exists_nat_one_div_lt

Modified algebra/field_power.lean

Modified analysis/limits.lean

added theorem tendsto_inverse_at_top_nhds_0_nat

added theorem tendsto_one_div_at_top_nhds_0_nat

Modified data/padics/padic_integers.lean

modified def padic_int.cau_seq_lim

deleted theorem padic_int.complete

Modified data/padics/padic_numbers.lean

modified def padic.cau_seq_lim

modified theorem padic.cau_seq_lim_spec

modified theorem padic.padic_norm_e_lim_le

Modified data/real/cau_seq_completion.lean

modified def cau_seq.completion.Cauchy

modified theorem cau_seq.completion.cau_seq_zero_ne_one

Modified data/real/cau_seq_filter.lean

added theorem cau_filter_lim_spec

added theorem cau_seq_lim_spec

added theorem cau_seq_of_cau_filter_mem_set_seq

added theorem complete_space_of_cauchy_complete

added theorem is_cau_seq_of_dist_tendsto_0

added theorem le_nhds_cau_seq_lim

added theorem mono_of_mono_succ

added theorem seq_of_cau_filter_is_cauchy'

added theorem seq_of_cau_filter_is_cauchy

added theorem seq_of_cau_filter_mem_set_seq

added def set_seq_of_cau_filter

added theorem set_seq_of_cau_filter_inhabited

added theorem set_seq_of_cau_filter_mem_sets

added theorem set_seq_of_cau_filter_monotone'

added theorem set_seq_of_cau_filter_monotone

added theorem set_seq_of_cau_filter_spec

added theorem tendsto_div