coprodAssoc_symm_apply_inl — Mathlib

English

Analogous statement for the mixed injection under the inverse associator: (coprodAssoc M N P).symm(inr(inl x)) = inl(inr x).

Русский

Аналогично для смешанного включения: (coprodAssoc).symm(inr(inl x)) = inl(inr x).

LaTeX

$$$ (coprodAssoc(M,N,P))^{-1}(inr(inl(x))) = inl(inr(x)) \quad (x\\in N). $$$

Lean4

@[to_additive (attr := simp)]
theorem coprodAssoc_symm_apply_inl (x : M) : (coprodAssoc M N P).symm (inl x) = inl (inl x) :=
  rfl

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