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 #

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]

def first_order.language.graph :

first_order.language

The language consisting of a single relation representing adjacency.

Equations

first_order.language.graph = first_order.language.mk₂ empty empty empty empty unit

Instances for first_order.language.graph

first_order.language.graph.first_order.language.is_relational

def first_order.language.adj :

first_order.language.graph.relations 2

The symbol representing the adjacency relation.

Equations

first_order.language.adj = unit.star()

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

first_order.language.graph.Structure V

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

Equations

G.Structure = first_order.language.Structure.mk₂ empty.elim empty.elim empty.elim empty.elim (λ (_x : unit), G.adj)

@[protected, instance]

def first_order.language.graph.first_order.language.is_relational :

first_order.language.graph.is_relational

@[protected, instance]

def first_order.language.graph.relations.subsingleton {n : ℕ} :

subsingleton (first_order.language.graph.relations n)

@[protected]

def first_order.language.Theory.simple_graph :

first_order.language.graph.Theory

The theory of simple graphs.

Equations

first_order.language.Theory.simple_graph = {first_order.language.adj.irreflexive, first_order.language.adj.symmetric}

Instances for first_order.language.Theory.simple_graph

first_order.language.simple_graph_model

@[simp]

theorem first_order.language.Theory.simple_graph_model_iff {V : Type w'} [first_order.language.graph.Structure V] :

V ⊨ first_order.language.Theory.simple_graph ↔ irreflexive (λ (x y : V), first_order.language.Structure.rel_map first_order.language.adj ![x, y]) ∧ symmetric (λ (x y : V), first_order.language.Structure.rel_map first_order.language.adj ![x, y])

@[protected, instance]

def first_order.language.simple_graph_model {V : Type w'} (G : simple_graph V) :

V ⊨ first_order.language.Theory.simple_graph

@[simp]

theorem first_order.language.simple_graph_of_structure_adj (V : Type w') [first_order.language.graph.Structure V] [V ⊨ first_order.language.Theory.simple_graph] (x y : V) :

(first_order.language.simple_graph_of_structure V).adj x y = first_order.language.Structure.rel_map first_order.language.adj ![x, y]

def first_order.language.simple_graph_of_structure (V : Type w') [first_order.language.graph.Structure V] [V ⊨ first_order.language.Theory.simple_graph] :

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

Equations

first_order.language.simple_graph_of_structure V = {adj := λ (x y : V), first_order.language.Structure.rel_map first_order.language.adj ![x, y], symm := _, loopless := _}

@[simp]

theorem simple_graph.simple_graph_of_structure {V : Type w'} (G : simple_graph V) :

first_order.language.simple_graph_of_structure V = G

@[simp]

theorem first_order.language.Structure_simple_graph_of_structure {V : Type w'} [S : first_order.language.graph.Structure V] [V ⊨ first_order.language.Theory.simple_graph] :

(first_order.language.simple_graph_of_structure V).Structure = S

theorem first_order.language.Theory.simple_graph_is_satisfiable :

first_order.language.Theory.simple_graph.is_satisfiable