Theorems · Definition · functional analysis
Seminorm.toAddGroupSeminorm
{𝕜 : Type u_12} →
{E : Type u_13} →
[inst : SeminormedRing 𝕜] → [inst_1 : AddGroup E] → [inst_2 : SMul 𝕜 E] → Seminorm 𝕜 E → AddGroupSeminorm E- Defined in
- Mathlib.Analysis.Seminorm
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- SeminormedRingAddGroupSMul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- SeminormedRingstatement and proof · cited by 446
- Seminormstatement and proof · cited by 272
- AddGroupSeminormstatement · cited by 50
Cited by12
Results whose statement or proof uses this declaration.
- Seminorm.compproof · cited by 53
- Seminorm.restrictScalarsproof · cited by 4
- SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInfstatement · cited by 3
- Seminorm.bound_of_continuousproof · cited by 2
- WithSeminorms.equicontinuous_TFAEproof · cited by 2
- Seminorm.ball_eq_metricstatement · cited by 2
- Seminorm.uniformSpace_eq_of_hasBasisstatement · cited by 1
- Seminorm.vadd_ballproof · cited by 1
- Seminorm.closedBall_eq_metricstatement · cited by 1
- SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInfstatement · cited by 1
- Seminorm.vadd_closedBallproof · cited by 0
- Seminorm.smul'statement · cited by 0