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

Definition df-tsms 18148
 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 12472) and g (df-gsum 13720), 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 18147 . 2 tsums
2 vw . . 3
3 vf . . 3
4 cvv 2948 . . 3
5 vs . . . 4
63cv 1651 . . . . . . 7
76cdm 4870 . . . . . 6
87cpw 3791 . . . . 5
9 cfn 7101 . . . . 5
108, 9cin 3311 . . . 4
11 vy . . . . . 6
125cv 1651 . . . . . 6
132cv 1651 . . . . . . 7
1411cv 1651 . . . . . . . 8
156, 14cres 4872 . . . . . . 7
16 cgsu 13716 . . . . . . 7 g
1713, 15, 16co 6073 . . . . . 6 g
1811, 12, 17cmpt 4258 . . . . 5 g
19 ctopn 13641 . . . . . . 7
2013, 19cfv 5446 . . . . . 6
21 vz . . . . . . . . 9
2221cv 1651 . . . . . . . . . . 11
2322, 14wss 3312 . . . . . . . . . 10
2423, 11, 12crab 2701 . . . . . . . . 9
2521, 12, 24cmpt 4258 . . . . . . . 8
2625crn 4871 . . . . . . 7
27 cfg 16682 . . . . . . 7
2812, 26, 27co 6073 . . . . . 6
29 cflf 17959 . . . . . 6
3020, 28, 29co 6073 . . . . 5
3118, 30cfv 5446 . . . 4 g
325, 10, 31csb 3243 . . 3 g
332, 3, 4, 4, 32cmpt2 6075 . 2 g
341, 33wceq 1652 1 tsums g
 Colors of variables: wff set class This definition is referenced by:  tsmsval2  18151
 Copyright terms: Public domain W3C validator