braiding_inv_fst

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.BinaryFan.braiding_inv_fst

English

Inverse braiding composes with s.fst to give t.snd.

Русский

Обратный браидинг компонуется с s.fst чтобы дать t.snd.

LaTeX

$$$$ (braiding\\ P\\ Q)^{\\mathrm{inv}} \\circ s.fst = t.snd. $$$$

Lean4

@[reassoc (attr := simp)]
theorem braiding_inv_fst : (braiding P Q).inv ≫ s.fst = t.snd :=
  P.conePointUniqueUpToIso_inv_comp _ ⟨.left⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru