Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-topfld Unicode version

Definition df-topfld 25598
 Description: A topological field is a field whose addition, multiplication and inverse are continuous. (Contributed by FL, 21-May-2012.)
Assertion
Ref Expression
df-topfld GId GId
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-topfld
StepHypRef Expression
1 ctopfld 25597 . 2
2 vg . . . . . . 7
32cv 1622 . . . . . 6
4 vh . . . . . . 7
54cv 1622 . . . . . 6
63, 5cop 3643 . . . . 5
7 cfld 21080 . . . . 5
86, 7wcel 1684 . . . 4
9 vj . . . . . . 7
109cv 1622 . . . . . 6
116, 10cop 3643 . . . . 5
12 ctrg 17838 . . . . 5
1311, 12wcel 1684 . . . 4
143crn 4690 . . . . . . . 8
15 cgi 20854 . . . . . . . . . 10 GId
163, 15cfv 5255 . . . . . . . . 9 GId
1716csn 3640 . . . . . . . 8 GId
1814, 17cdif 3149 . . . . . . 7 GId
1918, 18cxp 4687 . . . . . 6 GId GId
205, 19cres 4691 . . . . 5 GId GId
21 ctx 17255 . . . . . . 7
2210, 10, 21co 5858 . . . . . 6
23 ccn 16954 . . . . . 6
2422, 10, 23co 5858 . . . . 5
2520, 24wcel 1684 . . . 4 GId GId
268, 13, 25w3a 934 . . 3 GId GId
2726, 2, 4, 9coprab 5859 . 2 GId GId
281, 27wceq 1623 1 GId GId
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator