prod_add — Mathlib

English

The product is additive in the first factor: (μ + μ').prod ν = μ.prod ν + μ'.prod ν.

Русский

Произведение аддитивно по первой компоненте: (μ + μ') × ν = μ × ν + μ' × ν.

LaTeX

$$$(μ + μ').prod ν = μ.prod ν + μ'.prod ν$$$

Lean4

theorem prod_add (ν' : Measure β) [SFinite ν'] : μ.prod (ν + ν') = μ.prod ν + μ.prod ν' :=
  by
  simp_rw [← sum_sfiniteSeq ν, ← sum_sfiniteSeq ν', sum_add_sum, ← sum_sfiniteSeq μ, prod_sum, sum_add_sum]
  congr
  ext1 i
  refine prod_eq fun s t _ _ => ?_
  simp_rw [add_apply, prod_prod, left_distrib]

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