fst_toProd — Mathlib

English

Let M and N be monoids. For every element x in the coproduct M ∗ N, the first coordinate of its image under the canonical map to the product equals the first projection of x itself.

Русский

Пусть M и N — моноиды. Для каждого элемента x в копродукте M ∗ N первая компонента образа x под отображением в произведение равно первой проекции x.

LaTeX

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

Lean4

@[to_additive (attr := simp) fst_toProd]
theorem fst_toProd (x : M ∗ N) : (toProd x).1 = fst x := by rw [← fst_comp_toProd]; rfl

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