Mathlib Map

Theorems · Theorem · functional analysis

SeminormedAddGroup.dist_eq

∀ {E : Type u_8} [self : SeminormedAddGroup E] (x y : E), dist x y = ‖-x + y‖

The distance function is induced by the norm.

Defined in
Mathlib.Analysis.Normed.Group.Defs
Cited by
3 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
SeminormedAddGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

dist_eq_norm_neg_add · cited by 46dist_eq_norm_neg_addAddGroupSeminorm.toSeminormedAddCommGroup · cited by 8AddGroupSeminorm.toSemino…IsUltrametricDist.isNonarchimedean_norm · cited by 8IsUltrametricDist.isNonar…AddGroupNormClass.toNormedAddGroup · cited by 1AddGroupNormClass.toNorme…AddGroupSeminormClass.toSeminormedAddCommGroup · cited by 1AddGroupSeminormClass.toS…CauchySeq.norm_bddAbove · cited by 1CauchySeq.norm_bddAboveAddGroupNorm.toNormedAddGroup · cited by 0AddGroupNorm.toNormedAddG…NormedAddGroup.ofAddDist · cited by 0NormedAddGroup.ofAddDistNormedAddGroup.ofAddDist' · cited by 0NormedAddGroup.ofAddDist'NormedAddGroup.ofSeparation · cited by 0NormedAddGroup.ofSeparati…SeminormedAddCommGroup.ofAddDist · cited by 0SeminormedAddCommGroup.of…SeminormedAddCommGroup.ofAddDist' · cited by 0SeminormedAddCommGroup.of…Real · cited by 25697RealNorm.norm · cited by 5413Norm.normDist.dist · cited by 1539Dist.distSeminormedAddGroup · cited by 331SeminormedAddGroupSeminormedAddGroup.dist_eqCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by12

Results whose statement or proof uses this declaration.