Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tng Structured version   Unicode version

Definition df-tng 21083
 Description: Define a function that fills in the topology and metric components of a structure given a group and a norm on it. (Contributed by Mario Carneiro, 2-Oct-2015.)
Assertion
Ref Expression
df-tng toNrmGrp sSet sSet TopSet
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-tng
StepHypRef Expression
1 ctng 21077 . 2 toNrmGrp
2 vg . . 3
3 vf . . 3
4 cvv 3095 . . 3
52cv 1382 . . . . 5
6 cnx 14611 . . . . . . 7
7 cds 14688 . . . . . . 7
86, 7cfv 5578 . . . . . 6
93cv 1382 . . . . . . 7
10 csg 16034 . . . . . . . 8
115, 10cfv 5578 . . . . . . 7
129, 11ccom 4993 . . . . . 6
138, 12cop 4020 . . . . 5
14 csts 14612 . . . . 5 sSet
155, 13, 14co 6281 . . . 4 sSet
16 cts 14685 . . . . . 6 TopSet
176, 16cfv 5578 . . . . 5 TopSet
18 cmopn 18387 . . . . . 6
1912, 18cfv 5578 . . . . 5
2017, 19cop 4020 . . . 4 TopSet
2115, 20, 14co 6281 . . 3 sSet sSet TopSet
222, 3, 4, 4, 21cmpt2 6283 . 2 sSet sSet TopSet
231, 22wceq 1383 1 toNrmGrp sSet sSet TopSet
 Colors of variables: wff setvar class This definition is referenced by:  reldmtng  21130  tngval  21131
 Copyright terms: Public domain W3C validator