mathlib3 documentation

model_theory.graph

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 #

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

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

Equations