English
Let (G_i) be a family of additive structures indexed by I, where each G_i has a zero and the TwoUniqueSums property. Then the dependent finite-support function space DFinsupp(I, G_i) also has TwoUniqueSums.
Русский
Пусть семейство добавочных структур (G_i) индексировано множеством I, каждая G_i имеет ноль и свойство TwoUniqueSums. Тогда пространство зависимых функций с конечной поддержкой DFinsupp(I, G_i) также обладает свойством TwoUniqueSums.
LaTeX
$$$\forall I \; \forall (G_i)_{i \in I},\;\Big(\forall i \in I,\; \text{AddZeroClass}(G_i) \wedge \text{TwoUniqueSums}(G_i)\Big) \Rightarrow \text{TwoUniqueSums}\big(\mathrm{DFinsupp}_{i \in I} G_i\big)$$$
Lean4
instance {ι} (G : ι → Type*) [∀ i, AddZeroClass (G i)] [∀ i, TwoUniqueSums (G i)] : TwoUniqueSums (Π₀ i, G i) :=
TwoUniqueSums.of_injective_addHom DFinsupp.coeFnAddMonoidHom.toAddHom DFunLike.coe_injective inferInstance
