symmetry_snd — Mathlib

English

In the relatively representable setting, symmetry interacts with the snd and fst components as hf'.symmetry hg ≫ hg.snd f' = hf'.fst' g, expressing a compatibility of the symmetry morphism with the projections.

Русский

В контексте относительно представимого свойство симметрии взаимодействует с компонентами snd и fst так, что hf'.symmetry hg ≫ hg.snd f' = hf'.fst' g, что выражает совместимость симметрии с проекциям.

LaTeX

$$$ hf'.symmetry hg \\; \\gg \\; hg.snd f' = hf'.fst' g $$$

Lean4

@[reassoc (attr := simp)]
theorem symmetry_snd [Full F] [Faithful F] : hf'.symmetry hg ≫ hg.snd f' = hf'.fst' g := by simp [symmetry]

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