Commit 2023-05-25 11:24 56573ef9

View on Github →

feat: port ModelTheory.Graph (#3989)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Graph.lean

added theorem FirstOrder.Language.Theory.simpleGraph_isSatisfiable

added theorem FirstOrder.Language.Theory.simpleGraph_model_iff

added def FirstOrder.Language.adj

added def FirstOrder.Language.simpleGraphOfStructure

added theorem FirstOrder.Language.structure_simpleGraphOfStructure

added theorem SimpleGraph.simpleGraphOfStructure

added def SimpleGraph.structure