Theorems · Theorem · combinatorics
SimpleGraph.Reachable.map
∀ {V : Type u} {V' : Type v} {u v : V} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G'),
G.Reachable u v → G'.Reachable (f u) (f v)- Cited by
- 14 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Adjstatement · cited by 1,346
- SimpleGraph.Walkproof · cited by 915
- SimpleGraph.Reachablestatement and proof · cited by 141
- SimpleGraph.Homstatement and proof · cited by 139
- SimpleGraph.Walk.mapproof · cited by 66
- SimpleGraph.Reachable.elimproof · cited by 7
Cited by14
Results whose statement or proof uses this declaration.
- SimpleGraph.Reachable.monoproof · cited by 10
- SimpleGraph.Subgraph.connected_supproof · cited by 3
- SimpleGraph.Reachable.coe_subgraphMapproof · cited by 2
- SimpleGraph.induce_connected_of_patchesproof · cited by 2
- SimpleGraph.Subgraph.Connected.exists_verts_eq_connectedComponentSuppproof · cited by 1
- SimpleGraph.ConnectedComponent.maximal_connected_induce_suppproof · cited by 1
- SimpleGraph.ConnectedComponent.maximal_connected_toSubgraphproof · cited by 1
- SimpleGraph.Preconnected.sum_sup_edgeproof · cited by 1
- SimpleGraph.Iso.reachable_iffproof · cited by 1
- SimpleGraph.Reachable.sum_sup_edgeproof · cited by 1
- SimpleGraph.Reachable.coe_toSubgraphproof · cited by 1
- SimpleGraph.Subgraph.preconnected_iff_forall_exists_walk_subgraphproof · cited by 1