sumDualDistrib_inr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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