Commit 2022-09-11 19:22 27917391

View on Github →

feat(topology/uniform_space/compact_separated): drop unneeded assumptions (#16457) Lemmas in this file don't need [separated_space _] / is_separated _ assumption. Also add nhds_set versions of some lemmas.

Estimated changes

Modified src/topology/algebra/uniform_group.lean

Modified src/topology/nhds_set.lean

added theorem nhds_set_diagonal

Modified src/topology/subset_properties.lean

added theorem is_compact_diagonal

Modified src/topology/uniform_space/basic.lean

added theorem is_compact.nhds_set_basis_uniformity

deleted theorem mem_map_iff_exists_image'

modified theorem mem_uniformity_of_uniform_continuous_invariant

added theorem nhds_set_diagonal_le_uniformity

added theorem uniformity_prod_eq_comap_prod

Modified src/topology/uniform_space/compact_separated.lean

modified theorem compact_space.uniform_continuous_of_continuous

modified theorem compact_space_uniformity

modified theorem continuous.tendsto_uniformly

deleted theorem is_compact.uniform_continuous_on_of_continuous'

modified theorem is_compact.uniform_continuous_on_of_continuous

added theorem nhds_set_diagonal_eq_uniformity

added theorem unique_uniformity_of_compact

deleted theorem unique_uniformity_of_compact_t2