Structures · Analysis
SeminormedCommGroup
A seminormed group is a group endowed with a norm for which dist x y = ‖x⁻¹ * y‖
defines a pseudometric space structure.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Shape
- One type argument · adds dist_eq
Extends3
Extended by1
Forgetful instances
Concrete types that are instances6
- Subtype
- Prod
- OrderDual
- ULift
- HasQuotient.Quotient
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by219
- dist_eq_norm_div
- norm_inv_mul
- IsCompact.mul_closedBall_one
- singleton_mul_ball
- dist_mul_mul_le
- LipschitzOnWith.mul
- singleton_mul_closedBall
- inv_ball
- ball_mul_one
- mul_ball_one
- singleton_mul_sphere
- inv_closedBall
- Finset.Nonempty.norm_prod_le_sup'_norm
- closedBall_mul_singleton
- sphere_mul_singleton
- IsUltrametricDist.norm_tprod_le
- mul_ball
- infEDist_inv_inv
- nullSubgroup
- IsUltrametricDist.exists_norm_finsetProd_le_of_nonempty
- mem_ball_iff_norm''
- locallyLipschitzOn_inv_iff
- abs_norm_sub_norm_le'
- pow_mem_ball
- norm_prod_le_of_le
- mem_closedBall_iff_norm''
- smul_ball''
- norm_prod_le
- locallyLipschitz_inv_iff
- lipschitzOnWith_inv_iff
- IsCompact.mul_closedBall
- QuotientGroup.norm_lt_iff
- lipschitzWith_inv_iff
- preimage_mul_ball
- antilipschitzWith_inv_iff
- LocallyLipschitzOn.mul
- sphere_div_singleton
- norm_multiset_prod_le
- QuotientGroup.exists_norm_mk_lt
- LipschitzWith.inv
- LipschitzWith.mul
- abs_dist_sub_le_dist_mul_mul
- Finset.nnnorm_prod_le_sup_nnnorm
- closedBall_div_singleton
- QuotientGroup.norm_mk
- LocallyLipschitz.mul
- nnnorm_norm'
- ball_mul
- dist_div_div_le
- SeparationQuotient.norm_mk'
Ancestors64
- AlgebraicGeometry.QuasiSeparated
- Bornology
- CancelCommMonoid
- CancelMonoid
- ChartedSpace
- CommGroup
- CommMagma
- CommMonoid
- CommSemigroup
- CompactSpace
- CompactlyCoherentSpace
- Dist
- Div
- DivInvMonoid
- DivInvOneMonoid
- DivisionCommMonoid
- DivisionMonoid
- Dvd
- EDist
- ENorm
- Group
- HDiv
- HMul
- HSMul
- Inv
- InvOneClass
- InvolutiveInv
- IsLeftCancelMul
- IsRightCancelMul
- LeftCancelMonoid
- LeftCancelSemigroup
- LocallyPathConnectedSpace
- Monoid
- Mul
- MulAction
- MulOne
- MulOneClass
- NNDist
- NNNorm
- NPow
- NSMul
- Nonempty
- Norm
- OfNat
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- RightCancelMonoid
- RightCancelSemigroup
- SDiv
- SMul
- Semigroup
- SemigroupAction
- SeminormedGroup
- SequentialSpace
- TopologicalSpace
- Topology.IsGeneratedBy
- Torsor
- UniformSpace
- ZPow
- ZSMul
- Zero