Commit 2023-11-11 08:27 5f066e77

View on Github →

chore: generalize CauchySeq to Preorder (#8339)

Estimated changes

Modified Mathlib/Analysis/Normed/Group/InfiniteSum.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

modified theorem cauchySeq_finset_iff_tsum_vanishing

modified theorem cauchySeq_finset_iff_vanishing

modified theorem summable_iff_cauchySeq_finset

Modified Mathlib/Topology/Algebra/UniformGroup.lean

modified theorem CauchySeq.const_mul

modified theorem CauchySeq.inv

modified theorem CauchySeq.mul

modified theorem CauchySeq.mul_const

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

modified theorem CauchySeq.comp_tendsto

modified theorem CauchySeq.nonempty

modified theorem CauchySeq.prod

modified theorem CauchySeq.prod_map

modified theorem CauchySeq.tendsto_limUnder

modified theorem CauchySeq.tendsto_uniformity

modified def CauchySeq

modified theorem UniformContinuous.comp_cauchySeq

modified theorem cauchySeq_tendsto_of_complete

modified theorem cauchySeq_tendsto_of_isComplete

modified theorem tendsto_nhds_of_cauchySeq_of_subseq