fst_swap — Mathlib

English

Let x be an element of the coproduct M ∗ N. Then the first component of x after swapping the factors is the second component of x.

Русский

Пусть x — элемент копродукта M ∗ N. Тогда первая компонента x после перестановки факторов равна второй компоненте x.

LaTeX

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

Lean4

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

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