boxProdRight — Mathlib

English

Applying ofBoxProdLeft to a boxProdLeft-walk yields the original walk.

Русский

Применение ofBoxProdLeft к пути boxProdLeft возвращает исходный путь.

LaTeX

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

Lean4

/-- Turn a walk on `H` into a walk on `G □ H`. -/
protected def boxProdRight {b₁ b₂ : β} (a : α) : H.Walk b₁ b₂ → (G □ H).Walk (a, b₁) (a, b₂) :=
  Walk.map (G.boxProdRight H a).toHom

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