Metamath Proof Explorer

Definition df-ushgr

Description: Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the edge function e is an injective (one-to-one) function into subsets of the set of vertices v , representing the (one or more) vertices incident to the edge. This definition corresponds to the 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 subset of [... the power set of V, that is the set of all subsets of V" resp. "the elements of E are nonempty subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020) (Revised by AV, 8-Oct-2020)

|- USHGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) }

 |-  USHGraph

 |-  g

 |-  Vtx

 |-  g

 |-  ( Vtx ` g )

 |-  v

 |-  iEdg

 |-  ( iEdg ` g )

 |-  e

 |-  e

 |-  dom e

 |-  v

 |-  ~P v

 |-  (/)

 |-  { (/) }

 |-  ( ~P v \ { (/) } )

 |-  e : dom e -1-1-> ( ~P v \ { (/) } )

 |-  [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } )

 |-  [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } )

 |-  { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) }

 |-  USHGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) }