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 25546
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 25545 . 2  class convex
2 vf . . 3  set  f
3 cibg 25474 . . 3  class Ibg
4 vp . . . . . . . . 9  set  p
54cv 1618 . . . . . . . 8  class  p
6 vq . . . . . . . . 9  set  q
76cv 1618 . . . . . . . 8  class  q
82cv 1618 . . . . . . . . 9  class  f
9 cseg 25497 . . . . . . . . 9  class  seg
108, 9cfv 4673 . . . . . . . 8  class  ( seg `  f )
115, 7, 10co 5792 . . . . . . 7  class  ( p ( seg `  f
) q )
12 vx . . . . . . . 8  set  x
1312cv 1618 . . . . . . 7  class  x
1411, 13wss 3127 . . . . . 6  wff  ( p ( seg `  f
) q )  C_  x
1514, 6, 13wral 2518 . . . . 5  wff  A. q  e.  x  ( p
( seg `  f
) q )  C_  x
1615, 4, 13wral 2518 . . . 4  wff  A. p  e.  x  A. q  e.  x  ( p
( seg `  f
) q )  C_  x
17 cpoints 25423 . . . . . 6  class PPoints
188, 17cfv 4673 . . . . 5  class  (PPoints `  f
)
1918cpw 3599 . . . 4  class  ~P (PPoints `  f )
2016, 12, 19crab 2522 . . 3  class  { x  e.  ~P (PPoints `  f
)  |  A. p  e.  x  A. q  e.  x  ( p
( seg `  f
) q )  C_  x }
212, 3, 20cmpt 4051 . 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 1619 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