Theorems · Theorem · combinatorics
SimpleGraph.subgraphOfAdj_adj
∀ {V : Type u} (G : SimpleGraph V) {v w : V} (hvw : G.Adj v w) (a b : V),
(G.subgraphOfAdj hvw).Adj a b = (s(v, w) = s(a, b))- Cited by
- 14 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Adjstatement and proof · cited by 1,346
- Sym2statement · cited by 737
- Sym2.mkstatement · cited by 332
- SimpleGraph.Subgraph.Adjstatement and proof · cited by 147
- SimpleGraph.subgraphOfAdjstatement and proof · cited by 36
Cited by14
Results whose statement or proof uses this declaration.
- SimpleGraph.Walk.toSubgraph_adj_getVertproof · cited by 4
- SimpleGraph.Subgraph.subgraphOfAdj_connectedproof · cited by 3
- SimpleGraph.subgraphOfAdj_symmproof · cited by 2
- SimpleGraph.neighborSet_fst_subgraphOfAdjproof · cited by 2
- SimpleGraph.Subgraph.subgraphOfAdj_eq_induceproof · cited by 2
- SimpleGraph.Walk.toSubgraph_reverseproof · cited by 2
- SimpleGraph.edgeSet_subgraphOfAdjproof · cited by 1
- SimpleGraph.Subgraph.spanningCoe_subgraphOfAdjproof · cited by 1
- SimpleGraph.neighborSet_subgraphOfAdj_of_ne_of_neproof · cited by 1
- SimpleGraph.Subgraph.IsMatching.subgraphOfAdjproof · cited by 0
- SimpleGraph.support_subgraphOfAdjproof · cited by 0
- SimpleGraph.nonempty_hom_of_forall_finite_subgraph_homproof · cited by 0