First-Ordered Structures in Graph Theory #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines first-order languages, structures, and theories in graph theory.
Main Definitions #
The language consisting of a single relation representing adjacency.
The symbol representing the adjacency relation.
Any simple graph can be thought of as a structure in the language of graphs.
The theory of simple graphs.
Any model of the theory of simple graphs represents a simple graph.