Commit 2023-03-14 00:17 1c543ada

View on Github →

feat: port Topology.MetricSpace.CauSeqFilter (#2852)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/CauSeqFilter.lean

added theorem CauSeq.cauchySeq

added theorem CauSeq.tendsto_limit

added theorem CauchySeq.isCauSeq

added theorem cau_seq_iff_cauchySeq