coprodAssoc_apply_inl_inr — Mathlib

English

Similarly, coprodAssoc(inl(inr y)) = inr(inl y) for y ∈ N, expressing compatibility of the associator with the mixed injections.

Русский

Аналогично, coprodAssoc(inl(inr y)) = inr(inl y) для y ∈ N, выражая совместимость ассоциатора с смешанными включениями.

LaTeX

$$$ coprodAssoc( M,N,P )( inl( inr(y) ) ) = inr( inl(y) ) \quad (y \\in N). $$$

Lean4

@[to_additive (attr := simp)]
theorem coprodAssoc_apply_inl_inr (x : N) : coprodAssoc M N P (inl (inr x)) = inr (inl x) :=
  rfl

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