Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ushgr Structured version   Unicode version

Definition df-ushgr 32737
Description: Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph  <. V ,  E >. where  E is an injective (one-to-one) function into subsets of  V, representing the (one or more) vertices incident to the edge. This definition corresponds to definition of hypergraphs in section I.1 of [Bollobas] p. 7 (except that the empty set seems to be allowed to be an "edge") or section 1.10 of [Diestel] p. 27, where "E is a subsets of [...] the power set of V, that is the set of all subsets of V" resp. "the elements of E a (non-empty) subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020.)
Assertion
Ref Expression
df-ushgr  |- USHGraph  =  {
g  |  [. ( Base `  g )  / 
v ]. [. ( .ef  `  g )  /  e ]. e : dom  e -1-1-> ( ~P v  \  { (/) } ) }
Distinct variable group:    v, g, e

Detailed syntax breakdown of Definition df-ushgr
StepHypRef Expression
1 cushgr 32734 . 2  class USHGraph
2 ve . . . . . . . 8  setvar  e
32cv 1397 . . . . . . 7  class  e
43cdm 4988 . . . . . 6  class  dom  e
5 vv . . . . . . . . 9  setvar  v
65cv 1397 . . . . . . . 8  class  v
76cpw 3999 . . . . . . 7  class  ~P v
8 c0 3783 . . . . . . . 8  class  (/)
98csn 4016 . . . . . . 7  class  { (/) }
107, 9cdif 3458 . . . . . 6  class  ( ~P v  \  { (/) } )
114, 10, 3wf1 5567 . . . . 5  wff  e : dom  e -1-1-> ( ~P v  \  { (/) } )
12 vg . . . . . . 7  setvar  g
1312cv 1397 . . . . . 6  class  g
14 cedgf 32732 . . . . . 6  class .ef
1513, 14cfv 5570 . . . . 5  class  ( .ef  `  g )
1611, 2, 15wsbc 3324 . . . 4  wff  [. ( .ef  `  g )  /  e ]. e : dom  e -1-1-> ( ~P v  \  { (/) } )
17 cbs 14716 . . . . 5  class  Base
1813, 17cfv 5570 . . . 4  class  ( Base `  g )
1916, 5, 18wsbc 3324 . . 3  wff  [. ( Base `  g )  / 
v ]. [. ( .ef  `  g )  /  e ]. e : dom  e -1-1-> ( ~P v  \  { (/) } )
2019, 12cab 2439 . 2  class  { g  |  [. ( Base `  g )  /  v ]. [. ( .ef  `  g
)  /  e ]. e : dom  e -1-1-> ( ~P v  \  { (/)
} ) }
211, 20wceq 1398 1  wff USHGraph  =  {
g  |  [. ( Base `  g )  / 
v ]. [. ( .ef  `  g )  /  e ]. e : dom  e -1-1-> ( ~P v  \  { (/) } ) }
Colors of variables: wff setvar class
This definition is referenced by:  isushgr  32739
  Copyright terms: Public domain W3C validator