sumLexDualAntidistrib_inr — Mathlib

English

The symmetry of the dual antidistrib swaps the left and right components via the duality: (sumLexDualAntidistrib α β).symm (inl (toDual b)) = toDual (inr b).

Русский

Симметрия двойственного антираспределителя меняет левую и правую части через двойственность: (sumLexDualAntidistrib α β).symm (inl (toDual b)) = toDual (inr b).

LaTeX

$$$\\bigl(\\text{sumLexDualAntidistrib}_{\\alpha,\\beta}\\bigr)^{-1}(\\mathrm{inl}(\\mathrm{toDual}(b))) = \\mathrm{toDual}(\\mathrm{inr}(b))$$$

Lean4

@[simp]
theorem sumLexDualAntidistrib_inr : sumLexDualAntidistrib α β (toDual (inr b)) = inl (toDual b) :=
  rfl

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