Theorems · Theorem · general topology
Dilation.mk_coe_of_nndist_eq
∀ {α : Type u_5} {β : Type u_6} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (f : α →ᵈ β)
(h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y), Dilation.mkOfNNDistEq (⇑f) h = f- Defined in
- Mathlib.Topology.MetricSpace.Dilation
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- NNRealstatement and proof · cited by 4,310
- PseudoMetricSpacestatement and proof · cited by 1,550
- NNDist.nndiststatement and proof · cited by 235
- Dilationstatement and proof · cited by 44
- Dilation.extproof · cited by 8
- Dilation.mkOfNNDistEqstatement · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.