swap — Mathlib

English

If X and Y have a binary product, then Y and X have a binary product, constructed by swapping the legs of the limit cone.

Русский

Если у X и Y есть бинарный произведение, то у Y и X тоже есть бинарное произведение, получаемое обходом ножек лимитного конуса.

LaTeX

$$$$\\text{HasBinaryProduct}(Y,X) = \\langle \\text{BinaryFan.swap}(\\text{limit.cone}(\\text{pair}(X,Y))),\\; (\\text{limit.isLimit}(\\text{pair}(X,Y))).binaryFanSwap \\rangle.$$$$

Lean4

/-- Construct `HasBinaryProduct Y X` from `HasBinaryProduct X Y`.
This can't be an instance, as it would cause a loop in typeclass search. -/
theorem swap (X Y : C) [HasBinaryProduct X Y] : HasBinaryProduct Y X :=
  .mk ⟨BinaryFan.swap (limit.cone (pair X Y)), (limit.isLimit (pair X Y)).binaryFanSwap⟩

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