Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-20 23:53 6ae1b702

View on Github →

feat(topology/uniform_space/cauchy): add cauchy_seq.comp_injective (#11986) API changes:

add filter.at_top_le_cofinite;
add function.injective.nat_tendsto_at_top;
add cauchy_seq.comp_injective, function.bijective.cauchy_seq_comp_iff.

Estimated changes

Modified src/order/filter/cofinite.lean

added theorem at_top_le_cofinite

added theorem function.injective.nat_tendsto_at_top

modified theorem function.injective.tendsto_cofinite

Modified src/topology/uniform_space/cauchy.lean

added theorem cauchy_seq.comp_injective

added theorem function.bijective.cauchy_seq_comp_iff