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

Definition df-cusgr 40556
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 40668. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.)
Assertion
Ref Expression
df-cusgr ComplUSGraph = {𝑔 ∈ USGraph ∣ 𝑔 ∈ ComplGraph}

Detailed syntax breakdown of Definition df-cusgr
StepHypRef Expression
1 ccusgr 40551 . 2 class ComplUSGraph
2 vg . . . . 5 setvar 𝑔
32cv 1473 . . . 4 class 𝑔
4 ccplgr 40550 . . . 4 class ComplGraph
53, 4wcel 1975 . . 3 wff 𝑔 ∈ ComplGraph
6 cusgr 40377 . . 3 class USGraph
75, 2, 6crab 2895 . 2 class {𝑔 ∈ USGraph ∣ 𝑔 ∈ ComplGraph}
81, 7wceq 1474 1 wff ComplUSGraph = {𝑔 ∈ USGraph ∣ 𝑔 ∈ ComplGraph}
Colors of variables: wff setvar class
This definition is referenced by:  iscusgr  40638
  Copyright terms: Public domain W3C validator