sumDualDistrib_symm_inr — Mathlib

English

The inverse of sumDualDistrib on inr b is toDual (inr b): (sumDualDistrib α β).symm (inr (toDual b)) = toDual (inr b).

Русский

Обратное sumDualDistrib по правой части: (sumDualDistrib α β).symm (inr (toDual b)) = toDual (inr b).

LaTeX

$$$ (sumDualDistrib α β).symm (\mathrm{inr} (\mathrm{toDual} b)) = \mathrm{toDual} (\mathrm{inr} b) $$$

Lean4

@[simp]
theorem sumDualDistrib_symm_inr : (sumDualDistrib α β).symm (inr (toDual b)) = toDual (inr b) :=
  rfl

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