Commit 2023-02-27 13:07 353e8e50

View on Github →

feat: port Topology.Algebra.UniformGroup (#2480)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/UniformGroup.lean

added theorem CauchySeq.const_mul

added theorem CauchySeq.inv

added theorem CauchySeq.mul

added theorem CauchySeq.mul_const

added theorem DenseInducing.extend_Z_bilin

added theorem Filter.HasBasis.uniformity_of_nhds_one

added theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul

added theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul_swapped

added theorem Filter.HasBasis.uniformity_of_nhds_one_swapped

added theorem MonoidHom.uniformContinuous_of_continuousAt_one

added theorem TendstoUniformly.div

added theorem TendstoUniformly.mul

added theorem TendstoUniformlyOn.div

added theorem TendstoUniformlyOn.mul

added theorem TendstoUniformlyOnFilter.div

added theorem TendstoUniformlyOnFilter.mul

added theorem TopologicalGroup.t2Space_iff_one_closed

added theorem TopologicalGroup.t2Space_of_one_sep

added theorem TopologicalGroup.tendstoLocallyUniformlyOn_iff

added theorem TopologicalGroup.tendstoLocallyUniformly_iff

added theorem TopologicalGroup.tendstoUniformlyOn_iff

added theorem TopologicalGroup.tendstoUniformly_iff

added def TopologicalGroup.toUniformSpace

added theorem UniformCauchySeqOn.div

added theorem UniformCauchySeqOn.mul

added theorem UniformContinuous.div

added theorem UniformContinuous.inv

added theorem UniformContinuous.mul

added theorem UniformContinuous.pow_const

added theorem UniformContinuous.zpow_const

added theorem UniformGroup.ext

added theorem UniformGroup.ext_iff

added theorem UniformGroup.mk'

added theorem UniformGroup.toUniformSpace_eq

added theorem UniformGroup.uniformContinuous_iff_open_ker

added theorem UniformGroup.uniformity_countably_generated

added theorem comm_topologicalGroup_is_uniform

added theorem group_separationRel

added theorem tendsto_div_comap_self

added theorem topologicalGroup_is_uniform_of_compactSpace

added theorem totallyBounded_iff_subset_finite_unionᵢ_nhds_one

added theorem uniformContinuous_div

added theorem uniformContinuous_inv

added theorem uniformContinuous_monoidHom_of_continuous

added theorem uniformContinuous_mul

added theorem uniformContinuous_of_continuousAt_one

added theorem uniformContinuous_of_tendsto_one

added theorem uniformContinuous_pow_const

added theorem uniformContinuous_zpow_const

added theorem uniformEmbedding_translate_mul

added theorem uniformGroup_comap

added theorem uniformGroup_inf

added theorem uniformGroup_infᵢ

added theorem uniformGroup_infₛ

added theorem uniformity_eq_comap_inv_mul_nhds_one

added theorem uniformity_eq_comap_inv_mul_nhds_one_swapped

added theorem uniformity_eq_comap_nhds_one'

added theorem uniformity_eq_comap_nhds_one

added theorem uniformity_eq_comap_nhds_one_swapped

added theorem uniformity_translate_mul