coprodAssoc_apply_inr — Mathlib

English

The inverse of the associator respects the canonical inclusions in the symmetric direction, e.g., (coprodAssoc M N P).symm(inl x) = inl(inl x).

Русский

Обратный ассоциатор сохраняет включения в симметричном направлении: (coprodAssoc)^{-1}(inl x) = inl(inl x).

LaTeX

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

Lean4

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

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