Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 03:21 f1c98ba8

View on Github →

feat(topology/uniform_space/uniform_convergence_topology): define the uniform structure of uniform convergence (#13073)

Estimated changes

Modified src/topology/uniform_space/basic.lean

added theorem inf_uniformity'

added theorem infi_uniformity'

added theorem le_iff_uniform_continuous_id

Created src/topology/uniform_space/uniform_convergence_topology.lean

added theorem uniform_convergence.t2_space

added theorem uniform_convergence.uniform_continuous_eval

added theorem uniform_convergence_on.t2_space_of_covering

added theorem uniform_convergence_on.uniform_continuous_eval_of_mem