boxProd_adj — Mathlib

English

Adjacency in the box product is equivalent to the stated disjunction of adjacencies in G and H with coordinate matching.

Русский

Смежность в boxProd равносильна указанному дизъюкту смежности: либо первая компонента смежна в G и вторая координата совпадает, либо вторая компонента смежна в H и первая координата совпадает.

LaTeX

$$$\\\\forall {α β} {G : SimpleGraph α} {H : SimpleGraph β} {x y : α × β}, (G.boxProd H).Adj x y \\\\Longleftrightarrow G.Adj x.1 y.1 \\\\wedge x.2 = y.2 \\\\lor H.Adj x.2 y.2 \\\\wedge x.1 = y.1$$

Lean4

@[simp]
theorem boxProd_adj {x y : α × β} : (G □ H).Adj x y ↔ G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1 :=
  Iff.rfl

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