boxProd_adj_left — Mathlib

English

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

Русский

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

LaTeX

$$$\\\\forall {a_1 a_2 : α} {b : β}, ((G.boxProd H).Adj (a_1,b) (a_2,b)) \\\\Longleftrightarrow G.Adj a_1 a_2$$

Lean4

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

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