coe_dfinsuppSum — Mathlib

English

The coercion of the sum of a dependent family equals the sum of the coercions componentwise.

Русский

Сведение суммы зависимого семейства к сумме по компонентам совпадает с суммой по компонентам.

LaTeX

$$coe_dfinsuppSum (t : Π₀ i, γ i) (g : ∀ i, γ i → M →ₛₗ[σ₁₂] M₂) : ⇑(t.sum g) = t.sum fun i d => g i d$$

Lean4

theorem coe_dfinsuppSum (t : Π₀ i, γ i) (g : ∀ i, γ i → M →ₛₗ[σ₁₂] M₂) : ⇑(t.sum g) = t.sum fun i d => g i d :=
  rfl

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