Theorems · Theorem · functional analysis
Seminorm.gauge_ball
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (p : Seminorm ℝ E), gauge (p.ball 0 1) = ⇑pAny seminorm arises as the gauge of its unit ball.
- Defined in
- Mathlib.Analysis.Convex.Gauge
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites36
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setproof · cited by 53,352
- Realstatement and proof · cited by 25,697
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Set.ofPredproof · cited by 6,101
- mul_oneproof · cited by 3,885
- Set.Nonemptyproof · cited by 2,627
- LT.lt.leproof · cited by 2,189
- LT.lt.ne'proof · cited by 1,417
- InfSet.sInfproof · cited by 935
- mul_posproof · cited by 374
Cited by2
Results whose statement or proof uses this declaration.
- gauge_unit_ballproof · cited by 1
- Seminorm.gaugeSeminorm_ballproof · cited by 0