Theorems · Theorem · general topology

dist_smul_pair

∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] (x : α) (y₁ y₂ : β),
  dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂

Defined in

Mathlib.Topology.MetricSpace.Algebra

Cited by

5 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpacePseudoMetricSpaceZeroZeroSMulIsBoundedSMul