Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-11 11:52 2eba5241

View on Github →

chore(topology/algebra/uniform_group): use morphism classes (#13273)

Estimated changes

Modified src/topology/algebra/uniform_group.lean

modified theorem uniform_continuous_monoid_hom_of_continuous

added theorem uniform_continuous_of_continuous_at_one

modified theorem uniform_continuous_of_tendsto_one

modified theorem uniform_group.uniform_continuous_iff_open_ker