English
There is an induction principle for the elemental subalgebra generated by x: any property P that holds for x, is closed under star, algebra maps, addition and multiplication, and is preserved under closure, holds for all elements of elemental R x.
Русский
Для элементарной подалгебры существует принцип индукции: если свойство выполняется для x, замкнуто относительно операции звезды, алгебраических отображений, сложения и умножения и сохраняется при замыкании, то оно выполняется для всех элементов elemental(R,x).
LaTeX
$$$\text{Induction on subalgebra}$ (описано в виде условий) $\Rightarrow P(y,hy)$$$
Lean4
theorem tsupport_smul_subset_left {M α} [TopologicalSpace X] [Zero M] [Zero α] [SMulWithZero M α] (f : X → M)
(g : X → α) : (tsupport fun x => f x • g x) ⊆ tsupport f :=
closure_mono <| support_smul_subset_left f g
