boxProd_adj_right — Mathlib

English

If the two vertices share the same first coordinate, adjacency in boxProd reduces to adjacency in H on the second coordinates.

Русский

При одинаковой первой координате в boxProd смежность сводится к смежности в H по вторым координатам.

LaTeX

$$$\\\\forall {a : α} {b_1 b_2 : β}, ((G.boxProd H).Adj (a,b_1) (a,b_2)) \\\\Longleftrightarrow H.Adj b_1 b_2$$

Lean4

theorem boxProd_adj_right {a : α} {b₁ b₂ : β} : (G □ H).Adj (a, b₁) (a, b₂) ↔ H.Adj b₁ b₂ := by
  simp only [boxProd_adj, SimpleGraph.irrefl, false_and, and_true, false_or]

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