Structures · Analysis
SeminormedGroup
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 by2
Forgetful instances
Concrete types that are instances5
- Subtype
- Prod
- OrderDual
- ULift
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by271
- dist_eq_norm_inv_mul
- norm_inv'
- norm_nonneg'
- dist_one_right
- norm_mul_le'
- norm_one'
- dist_one_left
- approxOrderOf
- norm_le_pi_norm'
- dist_one
- pi_norm_le_iff_of_nonneg'
- continuous_norm'
- norm_pow_le_mul_norm
- nnnorm_inv'
- nnnorm_one'
- norm_div_le
- continuous_nnnorm'
- IsUltrametricDist.norm_mul_le_max
- nontrivialTopology_iff_exists_nnnorm_ne_zero'
- IsUltrametricDist.norm_mul_eq_max_of_norm_ne_norm
- dist_eq_norm_inv_mul'
- NormedGroup.nhds_basis_norm_lt
- norm_le_norm_add_norm_inv_mul
- tendsto_norm_inv_mul_self
- norm_mul_le_of_le'
- nndist_eq_nnnorm_inv_mul
- abs_norm_sub_norm_le_norm_inv_mul
- ofReal_norm'
- nontrivialTopology_iff_exists_norm_ne_zero'
- Filter.Tendsto.norm'
- isBounded_iff_forall_norm_le'
- MonoidHomClass.lipschitz_of_bound
- norm_div_rev
- Bornology.IsBounded.exists_norm_le'
- IsUltrametricDist.nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm
- comap_norm_atTop'
- IsUltrametricDist.nnnorm_pow_le
- indiscreteTopology_iff_forall_norm_eq_zero'
- norm_mul₃_le'
- dist_self_mul_right
- SeminormedGroup.dist_eq
- norm_mul_eq_norm_left
- mem_approxOrderOf_iff
- enorm_inv'
- norm_zpow_abs
- lipschitzOnWith_iff_norm_inv_mul_le
- norm_le_mul_norm_add'
- Isometry.norm_map_of_map_one
- norm_mul_eq_norm_right
- tendsto_norm_cobounded_atTop'
Ancestors57
- AlgebraicGeometry.QuasiSeparated
- Bornology
- CancelMonoid
- ChartedSpace
- CompactSpace
- CompactlyCoherentSpace
- Dist
- Div
- DivInvMonoid
- DivInvOneMonoid
- 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
- SequentialSpace
- TopologicalSpace
- Topology.IsGeneratedBy
- Torsor
- UniformSpace
- ZPow
- ZSMul
- Zero