sumDualDistrib_inl — Mathlib

English

The dual-distrib map sends inl a to inl a in dual. Specifically, sumDualDistrib α β (toDual (inl a)) = inl (toDual a).

Русский

Отображение распределения двойственности над левой частью переводит inl a в влево от двойственности: sumDualDistrib α β (toDual (inl a)) = inl (toDual a).

LaTeX

$$$\text{sumDualDistrib } \alpha \beta (\text{toDual}(\mathrm{inl} a)) = \mathrm{inl}(\text{toDual} a)$$$

Lean4

@[simp]
theorem sumDualDistrib_inl : sumDualDistrib α β (toDual (inl a)) = inl (toDual a) :=
  rfl

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