Theorems · Definition · combinatorics
SimpleGraph.map
{V : Type u_1} → {W : Type u_2} → (V → W) → SimpleGraph V → SimpleGraph WGiven a function, there is a covariant induced map on graphs by pushing forward
the adjacency relation.
This is injective when the function is (see SimpleGraph.map_injective).
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Maps
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.Adjproof · cited by 1,346
- Relation.Mapproof · cited by 40
Cited by54
Results whose statement or proof uses this declaration.
- SimpleGraph.spanningCoeproof · cited by 12
- SimpleGraph.Iso.mapstatement · cited by 6
- SimpleGraph.cliqueSet_mapstatement and proof · cited by 3
- SimpleGraph.comap_map_eqstatement · cited by 3
- SimpleGraph.extremalNumber_of_fintypeCard_eqproof · cited by 3
- SimpleGraph.map_le_iff_le_comapstatement and proof · cited by 3
- SimpleGraph.IsClique.mapstatement · cited by 3
- SimpleGraph.IsNClique.mapstatement and proof · cited by 2
- SimpleGraph.zarankiewicz_of_fintypeCard_eqproof · cited by 2
- SimpleGraph.comap_symmstatement · cited by 2
- SimpleGraph.Embedding.mapstatement · cited by 2
- SimpleGraph.isClique_map_iff_of_nontrivialstatement and proof · cited by 2