snd_swap

Mathlib.GroupTheory.Coprod.Basic

URI: https://scilib.ai/kg/mathlib#Monoid.Coprod.snd_swap

English

Let x be an element of the coproduct M ∗ N. Then snd (swap x) equals fst x.

Русский

Пусть x — элемент копродукта M ∗ N. Тогда snd (swap x) равно fst x.

LaTeX

$$$ \forall x \in M \ast N,\; \mathrm{snd}(\mathrm{swap}(x)) = \mathrm{fst}(x). $$$

Lean4

@[to_additive (attr := simp)]
theorem snd_swap (x : M ∗ N) : snd (swap M N x) = fst x :=
  lift_swap _ _ _

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

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

Разделы

Аффилиация

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