Theorems · Inductive type · combinatorics
SimpleGraph.Subgraph.Connected
{V : Type u} → {G : SimpleGraph V} → G.Subgraph → PropA subgraph is connected if it is connected when coerced to be a simple graph. Note: This is a structure to make it so one can be precise about how dot notation resolves.
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement · cited by 3,072
- SimpleGraph.Subgraphstatement · cited by 326
Cited by26
Results whose statement or proof uses this declaration.
- SimpleGraph.Subgraph.connected_iffstatement · cited by 5
- SimpleGraph.Subgraph.Connected.monostatement and proof · cited by 4
- SimpleGraph.connected_induce_iffstatement and proof · cited by 4
- SimpleGraph.Subgraph.Connected.coestatement and proof · cited by 4
- SimpleGraph.Subgraph.Connected.nonemptystatement and proof · cited by 3
- SimpleGraph.Subgraph.Connected.preconnectedstatement and proof · cited by 3
- SimpleGraph.Subgraph.subgraphOfAdj_connectedstatement · cited by 3
- SimpleGraph.Walk.toSubgraph_connectedstatement and proof · cited by 3
- SimpleGraph.Subgraph.connected_iff'statement and proof · cited by 3
- SimpleGraph.Subgraph.connected_supstatement · cited by 3
- SimpleGraph.ConnectedComponent.connected_toSubgraphstatement · cited by 2
- SimpleGraph.Subgraph.top_induce_pair_connected_of_adjstatement and proof · cited by 2