Commit 2023-08-08 18:01 275b475d

View on Github →

feat: basic facts about discrete subsets and subgroups (#5969)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/NormedSpace/Basic.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem MonoidHom.rangeRestrict_injective_iff

Modified Mathlib/GroupTheory/Subgroup/ZPowers.lean

added theorem Int.range_castAddHom

Modified Mathlib/Topology/Algebra/UniformGroup.lean

added theorem MonoidHom.tendsto_coe_cofinite_of_discrete

added theorem Subgroup.tendsto_coe_cofinite_of_discrete

Created Mathlib/Topology/DiscreteSubset.lean

added theorem Continuous.discrete_of_tendsto_cofinite_cocompact

added theorem IsClosed.tendsto_coe_cofinite_iff

added theorem IsClosed.tendsto_coe_cofinite_of_discreteTopology

added theorem tendsto_cofinite_cocompact_iff

added theorem tendsto_cofinite_cocompact_of_discrete

Modified Mathlib/Topology/Instances/Real.lean