Theorems · Inductive type · functional analysis
GroupSeminorm
(G : Type u_6) → [Group G] → Type u_6
A seminorm on a group G is a function f : G → ℝ that sends one to zero, is submultiplicative
and such that f x⁻¹ = f x for all x.
- Defined in
- Mathlib.Analysis.Normed.Group.Seminorm
- Cited by
- 39 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement · cited by 6,238
Cited by58
Results whose statement or proof uses this declaration.
- GroupSeminorm.compstatement and proof · cited by 9
- GroupSeminorm.toFunstatement and proof · cited by 8
- GroupSeminorm.extstatement and proof · cited by 7
- GroupNorm.toGroupSeminormstatement · cited by 2
- GroupSeminorm.coe_sSup_applystatement and proof · cited by 2
- GroupSeminorm.mk.injstatement · cited by 1
- GroupSeminorm.mk.noConfusionstatement · cited by 1
- QuotientGroup.groupSeminormstatement · cited by 1
- normGroupNormproof · cited by 1
- normGroupSeminormstatement · cited by 1
- GroupNorm.mk.injstatement and proof · cited by 1
- GroupNorm.mk.noConfusionstatement and proof · cited by 1