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

Definition df-tsms 20360
 Description: Define the set of limit points of an infinite group sum for the topological group . If is Hausdorff, then there will be at most one element in this set and tsums selects this unique element if it exists. tsums is a way to say that the sum exists and is unique. Note that unlike (df-sum 13468) and g (df-gsum 14694), this does not return the sum itself, but rather the set of all such sums, which is usually either empty or a singleton. (Contributed by Mario Carneiro, 2-Sep-2015.)
Assertion
Ref Expression
df-tsms tsums g
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-tsms
StepHypRef Expression
1 ctsu 20359 . 2 tsums
2 vw . . 3
3 vf . . 3
4 cvv 3113 . . 3
5 vs . . . 4
63cv 1378 . . . . . . 7
76cdm 4999 . . . . . 6
87cpw 4010 . . . . 5
9 cfn 7513 . . . . 5
108, 9cin 3475 . . . 4
11 vy . . . . . 6
125cv 1378 . . . . . 6
132cv 1378 . . . . . . 7
1411cv 1378 . . . . . . . 8
156, 14cres 5001 . . . . . . 7
16 cgsu 14692 . . . . . . 7 g
1713, 15, 16co 6282 . . . . . 6 g
1811, 12, 17cmpt 4505 . . . . 5 g
19 ctopn 14673 . . . . . . 7
2013, 19cfv 5586 . . . . . 6
21 vz . . . . . . . . 9
2221cv 1378 . . . . . . . . . . 11
2322, 14wss 3476 . . . . . . . . . 10
2423, 11, 12crab 2818 . . . . . . . . 9
2521, 12, 24cmpt 4505 . . . . . . . 8
2625crn 5000 . . . . . . 7
27 cfg 18178 . . . . . . 7
2812, 26, 27co 6282 . . . . . 6
29 cflf 20171 . . . . . 6
3020, 28, 29co 6282 . . . . 5
3118, 30cfv 5586 . . . 4 g
325, 10, 31csb 3435 . . 3 g
332, 3, 4, 4, 32cmpt2 6284 . 2 g
341, 33wceq 1379 1 tsums g
 Colors of variables: wff setvar class This definition is referenced by:  tsmsval2  20363
 Copyright terms: Public domain W3C validator