commSq — Mathlib

English

Every square in a category satisfies the commutativity condition: the two paths from the upper-left corner to the lower-right corner are equal.

Русский

Каждый квадрат в категории удовлетворяет условию коммутативности: два пути из верхнего левого угла в нижний правый совпадают.

LaTeX

$$$f_{24} \\circ f_{12} = f_{34} \\circ f_{13}$$$

Lean4

theorem commSq (sq : Square C) : CommSq sq.f₁₂ sq.f₁₃ sq.f₂₄ sq.f₃₄ where w := sq.fac

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