cons_product — Mathlib

English

Multiplying a left-cons cell with t distributes as the sum of maps: (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t.

Русский

Произведение левой константы с t распадается на сумму отображений в Prod.mk и произведения хвоста: (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t.

LaTeX

$$$(a ::ₘ s) \times^{\mathrm{SProd}} t = \mathrm{map}(\mathrm{Prod.mk}\ a)\ t + s \times^{\mathrm{SProd}} t$$$

Lean4

@[simp]
theorem cons_product : (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t := by simp [SProd.sprod, product]

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