Theorems · Theorem · logic and foundations

FirstOrder.Language.simpleGraphOfStructure_adj

∀ (V : Type u) [inst : FirstOrder.Language.graph.Structure V] [inst_1 : V ⊨ FirstOrder.Language.Theory.simpleGraph]
  (x y : V),
  (FirstOrder.Language.simpleGraphOfStructure V).Adj x y =
    FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]

Defined in: Mathlib.ModelTheory.Graph
Cited by: 0 results in Mathlib
Foundations: Depth 41 from the axioms · uses propext, Quot.sound
Assumes: FirstOrder.Language.Structure FirstOrder.Language.Theory.Model

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

SimpleGraph.Adjstatement and proof · cited by 1,346
Matrix.vecConsstatement · cited by 852
Matrix.vecEmptystatement · cited by 832
FirstOrder.Language.Structurestatement and proof · cited by 775
FirstOrder.Language.Structure.RelMapstatement · cited by 68
FirstOrder.Language.Theory.Modelstatement and proof · cited by 67
FirstOrder.Language.Theory.simpleGraphstatement and proof · cited by 4
FirstOrder.Language.graphstatement and proof · cited by 4
FirstOrder.Language.simpleGraphOfStructurestatement and proof · cited by 3
FirstOrder.Language.adjstatement · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.