Documentation

Mathlib.ModelTheory.Graph

First-Order Structures in Graph Theory #

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

Main Definitions #

Simple Graphs #

source
inductive FirstOrder.Language.graphRel :
ℕ → Type

The type of relations for the language of graphs, consisting of a single binary relation adj.

Instances For
    source
    instance FirstOrder.Language.instDecidableEqGraphRel {a✝ : ℕ} :
    DecidableEq (graphRel a✝)
    Equations
      source
      def FirstOrder.Language.graph :
      Language

      The language consisting of a single relation representing adjacency.

      Equations
        Instances For
          source
          instance FirstOrder.Language.instgraphIsRelational :
          Language.graph.IsRelational
          Equations
            source
            @[reducible, inline]
            abbrev FirstOrder.Language.adj :
            Language.graph.Relations 2

            The symbol representing the adjacency relation.

            Equations
              Instances For
                source
                def SimpleGraph.structure {V : Type u} (G : SimpleGraph V) :
                FirstOrder.Language.graph.Structure V

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

                Equations
                  Instances For
                    source
                    instance FirstOrder.Language.graph.instSubsingleton {n : ℕ} :
                    Subsingleton (Language.graph.Relations n)
                    source
                    def FirstOrder.Language.Theory.simpleGraph :
                    Language.graph.Theory

                    The theory of simple graphs.

                    Equations
                      Instances For
                        source
                        @[simp]
                        theorem FirstOrder.Language.Theory.simpleGraph_model_iff {V : Type u} [Language.graph.Structure V] :
                        V ⊨ Theory.simpleGraph ↔ (Irreflexive fun (x y : V) => Structure.RelMap adj ![x, y]) ∧ Symmetric fun (x y : V) => Structure.RelMap adj ![x, y]
                        source
                        instance FirstOrder.Language.simpleGraph_model {V : Type u} (G : SimpleGraph V) :
                        V ⊨ Theory.simpleGraph
                        source
                        def FirstOrder.Language.simpleGraphOfStructure (V : Type u) [Language.graph.Structure V] [V ⊨ Theory.simpleGraph] :
                        SimpleGraph V

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

                        Equations
                          Instances For
                            source
                            @[simp]
                            theorem FirstOrder.Language.simpleGraphOfStructure_adj (V : Type u) [Language.graph.Structure V] [V ⊨ Theory.simpleGraph] (x y : V) :
                            (simpleGraphOfStructure V).Adj x y = Structure.RelMap adj ![x, y]
                            source
                            @[simp]
                            theorem SimpleGraph.simpleGraphOfStructure {V : Type u} (G : SimpleGraph V) :
                            FirstOrder.Language.simpleGraphOfStructure V = G
                            source
                            @[simp]
                            theorem FirstOrder.Language.structure_simpleGraphOfStructure {V : Type u} [S : Language.graph.Structure V] [V ⊨ Theory.simpleGraph] :
                            (simpleGraphOfStructure V).structure = S
                            source
                            theorem FirstOrder.Language.Theory.simpleGraph_isSatisfiable :
                            Theory.simpleGraph.IsSatisfiable