English
The box product G □ H is the graph on α × β with adjacency given by: (a1,b1) adjacent to (a2,b2) iff a1 ~ a2 and b1 = b2, or a1 = a2 and b1 ~ b2.
Русский
Граф boxProd G □ H расположен на парном координатном пространстве α × β; смежность задаётся так: (a1,b1) ~ (a2,b2) тогда и только тогда, когда a1 ~ a2 и b1 = b2, или a1 = a2 и b1 ~ b2.
LaTeX
$$$G.boxProd(H)$ has Adj defined by $\\\\text{Adj}( (a_1,b_1), (a_2,b_2) ) \\\\Longleftrightarrow (G.Adj(a_1,a_2) \\\\wedge b_1 = b_2) \\\\lor (H.Adj(b_1,b_2) \\\\wedge a_1 = a_2)$$$
Lean4
/-- Box product of simple graphs. It relates `(a₁, b)` and `(a₂, b)` if `G` relates `a₁` and `a₂`,
and `(a, b₁)` and `(a, b₂)` if `H` relates `b₁` and `b₂`. -/
def boxProd (G : SimpleGraph α) (H : SimpleGraph β) : SimpleGraph (α × β)
where
Adj x y := G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1
symm x y := by simp [and_comm, eq_comm, adj_comm]
loopless x := by simp
