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

Definition df-cnvx 26179
Description: Definition of the convex subsets of points. Definition 24 of [AitkenIBG] p. 15. (For my private use only. Don't use.) (Contributed by FL, 5-Mar-2016.)
Assertion
Ref Expression
df-cnvx  |- convex  =  ( f  e. Ibg  |->  { x  e.  ~P (PPoints `  f
)  |  A. p  e.  x  A. q  e.  x  ( p
( seg `  f
) q )  C_  x } )
Distinct variable group:    x, f, p, q

Detailed syntax breakdown of Definition df-cnvx
StepHypRef Expression
1 cconvex 26178 . 2  class convex
2 vf . . 3  set  f
3 cibg 26107 . . 3  class Ibg
4 vp . . . . . . . . 9  set  p
54cv 1622 . . . . . . . 8  class  p
6 vq . . . . . . . . 9  set  q
76cv 1622 . . . . . . . 8  class  q
82cv 1622 . . . . . . . . 9  class  f
9 cseg 26130 . . . . . . . . 9  class  seg
108, 9cfv 5255 . . . . . . . 8  class  ( seg `  f )
115, 7, 10co 5858 . . . . . . 7  class  ( p ( seg `  f
) q )
12 vx . . . . . . . 8  set  x
1312cv 1622 . . . . . . 7  class  x
1411, 13wss 3152 . . . . . 6  wff  ( p ( seg `  f
) q )  C_  x
1514, 6, 13wral 2543 . . . . 5  wff  A. q  e.  x  ( p
( seg `  f
) q )  C_  x
1615, 4, 13wral 2543 . . . 4  wff  A. p  e.  x  A. q  e.  x  ( p
( seg `  f
) q )  C_  x
17 cpoints 26056 . . . . . 6  class PPoints
188, 17cfv 5255 . . . . 5  class  (PPoints `  f
)
1918cpw 3625 . . . 4  class  ~P (PPoints `  f )
2016, 12, 19crab 2547 . . 3  class  { x  e.  ~P (PPoints `  f
)  |  A. p  e.  x  A. q  e.  x  ( p
( seg `  f
) q )  C_  x }
212, 3, 20cmpt 4077 . 2  class  ( f  e. Ibg  |->  { x  e. 
~P (PPoints `  f )  |  A. p  e.  x  A. q  e.  x  ( p ( seg `  f ) q ) 
C_  x } )
221, 21wceq 1623 1  wff convex  =  ( f  e. Ibg  |->  { x  e.  ~P (PPoints `  f
)  |  A. p  e.  x  A. q  e.  x  ( p
( seg `  f
) q )  C_  x } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator