Theorems · Definition · functional analysis
AddGroupSeminorm.toSeminormedAddCommGroup
{E : Type u_5} → [inst : AddCommGroup E] → AddGroupSeminorm E → SeminormedAddCommGroup EConstruct a seminormed group from a seminorm, i.e., registering the pseudodistance
and the pseudometric space structure from the seminorm properties. Note that in most cases this
instance creates bad definitional equalities (e.g., it does not take into account a possibly
existing UniformSpace instance on E).
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- SeminormedAddCommGroupstatement · cited by 2,671
- SeminormedAddGroupproof · cited by 331
- AddGroupSeminormstatement and proof · cited by 50
- SeminormedAddGroup.dist_eqproof · cited by 3
- AddGroupSeminorm.toSeminormedAddGroupproof · cited by 1
Cited by10
Results whose statement or proof uses this declaration.
- 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.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
- RingSeminorm.toSeminormedRingproof · cited by 0
- InnerProductSpace.Core.toSeminormedAddCommGroupproof · cited by 0