ofBoxProdRight_boxProdRight — Mathlib

English

Compatibility of toDeleteEdges with boxProdLeft projection.

Русский

Совместимость toDeleteEdges с boxProdLeft.

LaTeX

$$$toDeleteEdges\\_boxProdLeft$$$

Lean4

@[simp]
theorem ofBoxProdRight_boxProdRight [DecidableEq α] [DecidableRel G.Adj] {a b₁ b₂ : α} :
    ∀ (w : G.Walk b₁ b₂), (w.boxProdRight G a).ofBoxProdRight = w
  | nil => rfl
  | cons' x y z h w =>
    by
    rw [Walk.boxProdRight, map_cons, ofBoxProdRight, Or.by_cases, dif_pos, ← Walk.boxProdRight]
    · simp [ofBoxProdRight_boxProdRight]
    · exact ⟨h, rfl⟩

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