Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-16 18:44 9fa14a60

View on Github →

feat(topology/uniform_space): properties of uniform convergence (#9958)

From the sphere eversion project
multiple proofs were golfed by @PatrickMassot
Probably some proofs can be golfed quite heavily Co-authored by: Patrick Massot patrickmassot@free.fr

Estimated changes

Modified src/logic/basic.lean

added theorem imp_forall_iff

Modified src/order/filter/basic.lean

added theorem filter.mem_prod_principal

added theorem filter.mem_prod_top

Modified src/topology/uniform_space/compact_separated.lean

added theorem continuous.tendsto_uniformly

added theorem continuous_on.tendsto_uniformly

Modified src/topology/uniform_space/separation.lean

added theorem is_separated.eq_of_uniform_continuous

added theorem is_separated.mono

added theorem is_separated.prod

Modified src/topology/uniform_space/uniform_convergence.lean

added theorem tendsto_prod_top_iff

added theorem tendsto_uniformly_iff_tendsto

added theorem tendsto_uniformly_on_iff_tendsto

added theorem uniform_continuous_on.tendsto_uniformly

added theorem uniform_continuous₂.tendsto_uniformly