Commit 2023-08-21 11:54 368923da

View on Github →

feat: behavior of Cauchy under operations on UniformSpace (#6694) Some of the lemmas are cherry-picked from leanprover-community/mathlib#17975 and will be useful for the general Arzela-Ascoli theorem, but I also filled some API holes on the way.

Estimated changes

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

added theorem Cauchy.mono_uniformSpace

added theorem cauchy_comap_uniformSpace

added theorem cauchy_iInf_uniformSpace'

added theorem cauchy_iInf_uniformSpace

added theorem cauchy_iff_le

added theorem cauchy_inf_uniformSpace

added theorem cauchy_prod_iff

Modified Mathlib/Topology/UniformSpace/Pi.lean

added theorem Cauchy.pi

added theorem Pi.uniformSpace_eq

added theorem cauchy_pi_iff'

added theorem cauchy_pi_iff