For each of these properties:
neighborSet/commonNeighbors/incidenceSet/edgeSetdegree/maxDegree/minDegree[e]dist/eccent/radius/[e]diam/[e]girth/center/ballReachable/Preconnected/Connected/IsAcyclic/IsTreeColoring/Colorable/chromaticNumcliqueNum/indepNumIsClique/IsIndepSetIsNClique/IsNIndepSetIsMaximumClique/IsMaximumIndepSetMaximal Clique/Maximal IndepSetCliqueFree/IndepSetFreeFreeadjMatrix/incMatrix/degMatrixIsEdgeReachable/IsEdgeConnected
add lemmas about how they are preserved through these operations:
Hom/Copy/Embedding/Iso_ ≤ _/_ ⊑ _/_ ⊴ __ ⊔ _/_ ⊓ _/_ \ __ᶜiSup/iInf⊤/⊥SimpleGraph.sum/boxProd
Some of these might require Disjoint G H or Disjoint G.support H.support or Surjective f, and in some only ≤/⊆ is possible instead of equality.
For each of these properties:
neighborSet/commonNeighbors/incidenceSet/edgeSetdegree/maxDegree/minDegree[e]dist/eccent/radius/[e]diam/[e]girth/center/ballReachable/Preconnected/Connected/IsAcyclic/IsTreeColoring/Colorable/chromaticNumcliqueNum/indepNumIsClique/IsIndepSetIsNClique/IsNIndepSetIsMaximumClique/IsMaximumIndepSetMaximal Clique/Maximal IndepSetCliqueFree/IndepSetFreeFreeadjMatrix/incMatrix/degMatrixIsEdgeReachable/IsEdgeConnectedadd lemmas about how they are preserved through these operations:
Hom/Copy/Embedding/Iso_ ≤ _/_ ⊑ _/_ ⊴ __ ⊔ _/_ ⊓ _/_ \ __ᶜiSup/iInf⊤/⊥SimpleGraph.sum/boxProdSome of these might require
Disjoint G HorDisjoint G.support H.supportorSurjective f, and in some only≤/⊆is possible instead of equality.