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

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

Detailed syntax breakdown of Definition df-Cut
StepHypRef Expression
1 ccut 25547 . 2 Cut
2 vf . . 3
3 cibg 25460 . . 3 Ibg
4 vx . . . 4
5 vy . . . 4
62cv 1618 . . . . . 6
7 cpoints 25409 . . . . . 6 PPoints
86, 7cfv 4659 . . . . 5 PPoints
98cpw 3585 . . . 4 PPoints
10 vu . . . . . . . . . 10
1110cv 1618 . . . . . . . . 9
12 vc . . . . . . . . . . 11
1312cv 1618 . . . . . . . . . 10
14 vv . . . . . . . . . . 11
1514cv 1618 . . . . . . . . . 10
16 cbtw 25459 . . . . . . . . . . 11 btw
176, 16cfv 4659 . . . . . . . . . 10 btw
1813, 15, 17co 5778 . . . . . . . . 9 btw
1911, 18wcel 1621 . . . . . . . 8 btw
2010, 4wel 1622 . . . . . . . . . 10
2114, 4wel 1622 . . . . . . . . . 10
2220, 21wa 360 . . . . . . . . 9
2310, 5wel 1622 . . . . . . . . . 10
2414, 5wel 1622 . . . . . . . . . 10
2523, 24wa 360 . . . . . . . . 9
2622, 25wo 359 . . . . . . . 8
2719, 26wi 6 . . . . . . 7 btw
284cv 1618 . . . . . . . 8
295cv 1618 . . . . . . . 8
3028, 29cun 3111 . . . . . . 7
3127, 14, 30wral 2516 . . . . . 6 btw
3231, 10, 30wral 2516 . . . . 5 btw
3332, 12, 30crab 2520 . . . 4 btw
344, 5, 9, 9, 33cmpt2 5780 . . 3 PPoints PPoints btw
352, 3, 34cmpt 4037 . 2 Ibg PPoints PPoints btw
361, 35wceq 1619 1 Cut Ibg PPoints PPoints btw
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator