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

Definition df-slices 26193
 Description: Return the slices generated by the Dedekind cut of a set of points. Definition 1 of [AitkenNG] p. 2. (For my private use only. Don't use.) (Contributed by FL, 5-Mar-2016.)
Assertion
Ref Expression
df-slices slices Ibg PPoints convex convex
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-slices
StepHypRef Expression
1 cslices 26192 . 2 slices
2 vf . . 3
3 cibg 26107 . . 3 Ibg
4 vx . . . 4
52cv 1622 . . . . . 6
6 cpoints 26056 . . . . . 6 PPoints
75, 6cfv 5255 . . . . 5 PPoints
87cpw 3625 . . . 4 PPoints
9 va . . . . . . . . . 10
109cv 1622 . . . . . . . . 9
11 vb . . . . . . . . . 10
1211cv 1622 . . . . . . . . 9
1310, 12cun 3150 . . . . . . . 8
144cv 1622 . . . . . . . 8
1513, 14wceq 1623 . . . . . . 7
1610, 12cin 3151 . . . . . . . 8
17 c0 3455 . . . . . . . 8
1816, 17wceq 1623 . . . . . . 7
1915, 18wa 358 . . . . . 6
2010, 17wne 2446 . . . . . . 7
2112, 17wne 2446 . . . . . . 7
2220, 21wa 358 . . . . . 6
23 cconvex 26178 . . . . . . . . 9 convex
245, 23cfv 5255 . . . . . . . 8 convex
2510, 24wcel 1684 . . . . . . 7 convex
2612, 24wcel 1684 . . . . . . 7 convex
2725, 26wa 358 . . . . . 6 convex convex
2819, 22, 27w3a 934 . . . . 5 convex convex
2928, 9, 11copab 4076 . . . 4 convex convex
304, 8, 29cmpt 4077 . . 3 PPoints convex convex
312, 3, 30cmpt 4077 . 2 Ibg PPoints convex convex
321, 31wceq 1623 1 slices Ibg PPoints convex convex
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator