# mathlibdocumentation

model_theory.graph

# First-Ordered Structures in Graph Theory #

This file defines first-order languages, structures, and theories in graph theory.

## Main Definitions #

• first_order.language.graph is the language consisting of a single relation representing adjacency.
• simple_graph.Structure is the first-order structure corresponding to a given simple graph.
• first_order.language.Theory.simple_graph is the theory of simple graphs.
• first_order.language.simple_graph_of_structure gives the simple graph corresponding to a model of the theory of simple graphs.

### Simple Graphs #

@[protected]

The language consisting of a single relation representing adjacency.

Equations
Instances for first_order.language.graph

The symbol representing the adjacency relation.

Equations
def simple_graph.Structure {V : Type w'} (G : simple_graph V) :

Any simple graph can be thought of as a structure in the language of graphs.

Equations
@[protected, instance]
@[protected, instance]
@[protected]

The theory of simple graphs.

Equations
Instances for first_order.language.Theory.simple_graph
@[simp]
theorem first_order.language.Theory.simple_graph_model_iff {V : Type w'}  :
irreflexive (λ (x y : V), symmetric (λ (x y : V),
@[protected, instance]
@[simp]
theorem first_order.language.simple_graph_of_structure_adj (V : Type w') (x y : V) :

Any model of the theory of simple graphs represents a simple graph.

Equations
@[simp]
theorem simple_graph.simple_graph_of_structure {V : Type w'} (G : simple_graph V) :
@[simp]