Theorems · Theorem · general topology

nndist_div_left

∀ {G : Type v} [inst : Group G] [inst_1 : PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G]
  (a b c : G), nndist (a / b) (a / c) = nndist b c

Defined in

Mathlib.Topology.MetricSpace.IsometricSMul

Cited by

0 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupPseudoMetricSpaceIsIsometricSMulIsIsometricSMul