Commit 2024-02-27 23:07 5d73e334

View on Github →

chore(Cauchy): drop Nonempty/Inhabited assumptions (#10871) Use haveI to drop unneeded Nonempty/Inhabited assumptions.

Estimated changes

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

modified theorem Cauchy.le_nhds_lim

modified theorem CauchySeq.tendsto_limUnder

Modified Mathlib/Topology/UniformSpace/Completion.lean

modified theorem CauchyFilter.cauchyFilter_eq