boxProd — Mathlib

English

If G and H are preconnected graphs, then their box product G □ H is preconnected.

Русский

Пусть графы G и H являются предсвязными; тогда их box-продукт G □ H тоже является предсвязным.

LaTeX

$$$\\text{Preconnected}(G) \\wedge \\text{Preconnected}(H) \\Rightarrow \\text{Preconnected}(G \\square H)$$$

Lean4

protected theorem boxProd (hG : G.Preconnected) (hH : H.Preconnected) : (G □ H).Preconnected :=
  by
  rintro x y
  obtain ⟨w₁⟩ := hG x.1 y.1
  obtain ⟨w₂⟩ := hH x.2 y.2
  exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩

Похожие утверждения