Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-25 11:49 8b7251cf

View on Github →

chore(topology/uniform_space/uniform_convergence_topology): use type aliases (#17516)

Estimated changes

Modified src/topology/algebra/module/strong_topology.lean

Modified src/topology/algebra/uniform_convergence.lean

deleted structure of

deleted theorem uniform_convergence_on.has_continuous_smul_induced_of_image_bounded

deleted theorem uniform_convergence_on.has_continuous_smul_submodule_of_image_bounded

added theorem uniform_on_fun.has_continuous_smul_induced_of_image_bounded

added theorem uniform_on_fun.has_continuous_smul_submodule_of_image_bounded

Modified src/topology/uniform_space/uniform_convergence_topology.lean

deleted theorem uniform_convergence.t2_space

deleted theorem uniform_convergence.uniform_continuous_eval

deleted theorem uniform_convergence_on.t2_space_of_covering

deleted theorem uniform_convergence_on.uniform_continuous_eval_of_mem

added def uniform_fun.of_fun

added def uniform_fun.to_fun

added theorem uniform_fun.uniform_continuous_eval

added def uniform_fun

added def uniform_on_fun.of_fun

added theorem uniform_on_fun.t2_space_of_covering

added def uniform_on_fun.to_fun

added theorem uniform_on_fun.uniform_continuous_eval_of_mem

added def uniform_on_fun