English
There is an induction principle for element z ∈ ⨂[R] i, s_i using scaled versions of tprod: if a property holds for all smul of tprod by scalars and is preserved by addition, then it holds for all z.
Русский
Существует индуктивный принцип для z ∈ ⨂[R] i, s_i, используя масштабируемые версии tprod: если свойство верно для всех скалярно умноженных на tprod и сохраняется при сложении, то оно верно для всех z.
LaTeX
$$$$ \forall z,\; (\forall r,f, P(r \cdot tprod(R,f)) ) \land (\forall x,y, P(x) \land P(y) \rightarrow P(x+y)) \rightarrow P(z) $$$$
Lean4
/-- If elements `p,q` of `FreeAddMonoid (R × Π i, s i)` lift elements `x,y` of `⨂[R] i, s i`
respectively, then `p + q` lifts `x + y`.
-/
theorem lifts_add {x y : ⨂[R] i, s i} {p q : FreeAddMonoid (R × Π i, s i)} (hp : p ∈ lifts x) (hq : q ∈ lifts y) :
p + q ∈ lifts (x + y) := by
simp only [lifts, Set.mem_setOf_eq, AddCon.coe_add]
rw [hp, hq]
