neighborSet_boxProd — Mathlib

English

The neighbor set of (a,b) in G □ H is the union of neighbors of a in G with second coordinate fixed at b, and neighbors of b in H with first coordinate fixed at a.

Русский

Множество соседей (a,b) в G□H есть сумма соседей a в G с фиксированной второй координатой b и соседей b в H с фиксированной первой координатой a.

LaTeX

$$$$(G.boxProd H).neighborSet (a,b) = G.neighborSet a \\\\times\\{b\\} \\cup \\{a\\} \\\\times H.neighborSet b$$$$

Lean4

theorem neighborSet_boxProd (x : α × β) :
    (G □ H).neighborSet x = G.neighborSet x.1 ×ˢ { x.2 } ∪ { x.1 } ×ˢ H.neighborSet x.2 :=
  by
  ext ⟨a', b'⟩
  simp only [mem_neighborSet, Set.mem_union, boxProd_adj, Set.mem_prod, Set.mem_singleton_iff]
  simp only [eq_comm, and_comm]

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