MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-metu Structured version   Visualization version   GIF version

Definition df-metu 20596
Description: Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
Assertion
Ref Expression
df-metu metUnif = (𝑑 ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (𝑑 “ (0[,)𝑎)))))
Distinct variable group:   𝑎,𝑑

Detailed syntax breakdown of Definition df-metu
StepHypRef Expression
1 cmetu 20588 . 2 class metUnif
2 vd . . 3 setvar 𝑑
3 cpsmet 20581 . . . . 5 class PsMet
43crn 5590 . . . 4 class ran PsMet
54cuni 4839 . . 3 class ran PsMet
62cv 1538 . . . . . . 7 class 𝑑
76cdm 5589 . . . . . 6 class dom 𝑑
87cdm 5589 . . . . 5 class dom dom 𝑑
98, 8cxp 5587 . . . 4 class (dom dom 𝑑 × dom dom 𝑑)
10 va . . . . . 6 setvar 𝑎
11 crp 12730 . . . . . 6 class +
126ccnv 5588 . . . . . . 7 class 𝑑
13 cc0 10871 . . . . . . . 8 class 0
1410cv 1538 . . . . . . . 8 class 𝑎
15 cico 13081 . . . . . . . 8 class [,)
1613, 14, 15co 7275 . . . . . . 7 class (0[,)𝑎)
1712, 16cima 5592 . . . . . 6 class (𝑑 “ (0[,)𝑎))
1810, 11, 17cmpt 5157 . . . . 5 class (𝑎 ∈ ℝ+ ↦ (𝑑 “ (0[,)𝑎)))
1918crn 5590 . . . 4 class ran (𝑎 ∈ ℝ+ ↦ (𝑑 “ (0[,)𝑎)))
20 cfg 20586 . . . 4 class filGen
219, 19, 20co 7275 . . 3 class ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (𝑑 “ (0[,)𝑎))))
222, 5, 21cmpt 5157 . 2 class (𝑑 ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (𝑑 “ (0[,)𝑎)))))
231, 22wceq 1539 1 wff metUnif = (𝑑 ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (𝑑 “ (0[,)𝑎)))))
Colors of variables: wff setvar class
This definition is referenced by:  metuval  23705
  Copyright terms: Public domain W3C validator