This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cusgr

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 . (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 24-Oct-2020) (Revised by BJ, 14-Feb-2022)

		Ref	Expression
	Assertion	df-cusgr	$⊢ ComplUSGraph = USGraph \cap ComplGraph$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccusgr	$class ComplUSGraph$
1		cusgr	$class USGraph$
2		ccplgr	$class ComplGraph$
3	1 2	cin	$class (USGraph \cap ComplGraph)$
4	0 3	wceq	$wff ComplUSGraph = USGraph \cap ComplGraph$