MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cusgr Structured version   Visualization version   GIF version

Definition df-cusgr 27196
Description: Define the class of all complete simple graphs. A simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge, see definition in section 1.1 of [Diestel] p. 3. In contrast, the definition in section I.1 of [Bollobas] p. 3 is based on the size of (finite) complete graphs, see cusgrsize 27238. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.) (Revised by BJ, 14-Feb-2022.)
Assertion
Ref Expression
df-cusgr ComplUSGraph = (USGraph ∩ ComplGraph)

Detailed syntax breakdown of Definition df-cusgr
StepHypRef Expression
1 ccusgr 27194 . 2 class ComplUSGraph
2 cusgr 26936 . . 3 class USGraph
3 ccplgr 27193 . . 3 class ComplGraph
42, 3cin 3937 . 2 class (USGraph ∩ ComplGraph)
51, 4wceq 1537 1 wff ComplUSGraph = (USGraph ∩ ComplGraph)
Colors of variables: wff setvar class
This definition is referenced by:  iscusgr  27202
  Copyright terms: Public domain W3C validator