ofBoxProdLeft_boxProdLeft — Mathlib

English

For w : G.Walk a₁ a₂, (w.boxProdLeft H b).ofBoxProdLeft = w.

Русский

Для пути w: G.Walk a₁ a₂ выполняется равенство.

LaTeX

$$$\\\\forall {a₁ a₂} {b} (w : G.Walk a₁ a₂), (w.boxProdLeft H b).ofBoxProdLeft = w$$

Lean4

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

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