Mathlib Map

Theorems · Theorem · general topology

nndist_div_right

∀ {M : Type u} [inst : DivInvMonoid M] [inst_1 : PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M),
  nndist (a / c) (b / c) = nndist a b
Defined in
Mathlib.Topology.MetricSpace.IsometricSMul
Cited by
0 results in Mathlib
Foundations
Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DivInvMonoidPseudoMetricSpaceIsIsometricSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

NNReal · cited by 4310NNRealPseudoMetricSpace · cited by 1550PseudoMetricSpaceMulOpposite · cited by 1135MulOppositediv_eq_mul_inv · cited by 715div_eq_mul_invNNDist.nndist · cited by 235NNDist.nndistDivInvMonoid · cited by 103DivInvMonoidIsIsometricSMul · cited by 74IsIsometricSMulnndist_mul_right · cited by 1nndist_mul_rightnndist_div_rightCITED BYCITES

Cites8

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

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.