Theorems · Theorem · Lie groups
isUniformAddGroup_of_addCommGroup
∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
IsUniformAddGroup G- Cited by
- 21 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites31
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- AddCommGroupstatement and proof · cited by 12,871
- nhdsproof · cited by 5,554
- Filter.Tendstoproof · cited by 3,814
- add_zeroproof · cited by 2,707
- add_commproof · cited by 1,535
- IsTopologicalAddGroupstatement and proof · cited by 1,394
- sub_eq_add_negproof · cited by 1,023
- neg_negproof · cited by 960
- Filter.mapproof · cited by 819
- add_assocproof · cited by 746
- Filter.Tendsto.compproof · cited by 560
Cited by21
Results whose statement or proof uses this declaration.
- FiniteDimensional.of_locallyCompactSpaceproof · cited by 7
- UniformConvergenceCLM.hasBasis_nhds_zero_of_basisproof · cited by 5
- Seminorm.continuous_of_continuousAt_zeroproof · cited by 4
- ContinuousMultilinearMap.hasBasis_nhds_zero_of_basisproof · cited by 3
- PointwiseConvergenceCLM.isEmbedding_coeFnproof · cited by 3
- Disjoint.exists_open_convexesproof · cited by 2
- UniformConvergenceCLM.nhds_zero_eq_of_basisproof · cited by 2
- Summable.vanishingproof · cited by 2
- bernsteinApproximation_uniformproof · cited by 1
- Summable.nat_tsum_vanishingproof · cited by 1
- AddGroupFilterBasis.isUniformAddGroupproof · cited by 1
- Summable.tsum_vanishingproof · cited by 1