Graph

📁 Source: Mathlib/ModelTheory/Graph.lean

Statistics

Metric	Count
Definitions simpleGraph, adj, graph, graphRel, instDecidableEqGraphRel, decEq, instIsRelationalGraph, simpleGraphOfStructure, Graph, Graph, structure	11
Theorems simpleGraph_isSatisfiable, simpleGraph_model_iff, instSubsingleton, simpleGraphOfStructure_adj, simpleGraph_model, structure_simpleGraphOfStructure, simpleGraphOfStructure	7
Total	18

FirstOrder.Language

Definitions

Name	Category	Theorems
adj 📖	CompOp	2 math math: simpleGraphOfStructure_adj, Theory.simpleGraph_model_iff
graph 📖	CompOp	5 math math: graph.instSubsingleton, simpleGraph_model, Theory.simpleGraph_isSatisfiable, simpleGraphOfStructure_adj, Theory.simpleGraph_model_iff
graphRel 📖	CompData	—
instDecidableEqGraphRel 📖	CompOp	—
instIsRelationalGraph 📖	CompOp	—
simpleGraphOfStructure 📖	CompOp	3 math math: SimpleGraph.simpleGraphOfStructure, simpleGraphOfStructure_adj, structure_simpleGraphOfStructure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
simpleGraphOfStructure_adj 📖	mathematical	—	SimpleGraph.Adj simpleGraphOfStructure Structure.RelMap graph adj Matrix.vecCons Matrix.vecEmpty	—	—
simpleGraph_model 📖	mathematical	—	Theory.Model graph SimpleGraph.structure Theory.simpleGraph	—	Theory.simpleGraph_model_iff SimpleGraph.loopless SimpleGraph.symm
structure_simpleGraphOfStructure 📖	mathematical	—	SimpleGraph.structure simpleGraphOfStructure	—	Structure.ext iff_eq_eq Matrix.cons_val_fin_one

FirstOrder.Language.Theory

Definitions

Name	Category	Theorems
simpleGraph 📖	CompOp	3 math math: FirstOrder.Language.simpleGraph_model, simpleGraph_isSatisfiable, simpleGraph_model_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
simpleGraph_isSatisfiable 📖	mathematical	—	IsSatisfiable FirstOrder.Language.graph simpleGraph	—	FirstOrder.Language.simpleGraph_model
simpleGraph_model_iff 📖	mathematical	—	Model FirstOrder.Language.graph simpleGraph FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj Matrix.vecCons Matrix.vecEmpty Symmetric	—	—

FirstOrder.Language.graph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSubsingleton 📖	mathematical	—	FirstOrder.Language.Relations FirstOrder.Language.graph	—	—

FirstOrder.Language.instDecidableEqGraphRel

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

Mathlib.Tactic.Order

Definitions

Name	Category	Theorems
Graph 📖	CompOp	—

SimpleGraph

Definitions

Name	Category	Theorems
structure 📖	CompOp	3 math math: simpleGraphOfStructure, FirstOrder.Language.simpleGraph_model, FirstOrder.Language.structure_simpleGraphOfStructure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
simpleGraphOfStructure 📖	mathematical	—	FirstOrder.Language.simpleGraphOfStructure structure FirstOrder.Language.simpleGraph_model	—	ext FirstOrder.Language.simpleGraph_model

(root)

Definitions

Name	Category	Theorems
Graph 📖	CompData	—

---

← Back to Index