Mathlib Map

Theorems · Definition · combinatorics

SimpleGraph.Subgraph.Adj

{V : Type u} → {G : SimpleGraph V} → G.Subgraph → V → V → Prop

Edges of the subgraph

Defined in
Mathlib.Combinatorics.SimpleGraph.Subgraph
Cited by
147 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SimpleGraph.Subgraph.coe · cited by 89Subgraph.coeSimpleGraph.Subgraph.neighborSet · cited by 46Subgraph.neighborSetSimpleGraph.Subgraph.ext · cited by 33Subgraph.extSimpleGraph.Subgraph.induce · cited by 33Subgraph.induceSimpleGraph.Subgraph.spanningCoe · cited by 33Subgraph.spanningCoeSimpleGraph.Subgraph.IsMatching · cited by 32Subgraph.IsMatchingSimpleGraph.Subgraph.map · cited by 24Subgraph.mapSimpleGraph.Subgraph.adj_sub · cited by 19Subgraph.adj_subSimpleGraph.Subgraph.edge_vert · cited by 17Subgraph.edge_vertSimpleGraph.Subgraph.induce_adj · cited by 17Subgraph.induce_adjSimpleGraph.subgraphOfAdj_adj · cited by 14SimpleGraph.subgraphOfAdj…SimpleGraph.Subgraph.Adj.symm · cited by 14Adj.symmSimpleGraph.Subgraph.deleteEdges · cited by 13Subgraph.deleteEdgesSimpleGraph.Subgraph.coe_adj · cited by 12Subgraph.coe_adjSimpleGraph.Subgraph.map_adj · cited by 10Subgraph.map_adjSimpleGraph · cited by 3072SimpleGraphSimpleGraph.Subgraph · cited by 326SimpleGraph.SubgraphSubgraph.AdjCITED BYCITES

Cites2

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

Cited by159

Results whose statement or proof uses this declaration.