English
An induction principle: if a property p holds for all elements of s and is preserved under addition, multiplication, scalar action, star, and contains 0, then p holds for all elements of adjoin R s.
Русский
Принцип индукции над adjoin: если свойство p верно для элементов s и сохраняется при сложении, умножении, действии на скаляр, операции звезды и нулем, то оно верно и для всех элементов adjoin R s.
LaTeX
$$$$ \\text{adjoin}_R(s) \\text{ satisfies induction: if } p \\text{ is closed under +, *, 0, r \\cdot -, star, and contains s, then } p(a) \\text{ for all } a \\in \\operatorname{adjoin}_R(s). $$$$
Lean4
@[elab_as_elim]
theorem adjoin_induction {s : Set A} {p : (x : A) → x ∈ adjoin R s → Prop}
(mem : ∀ (x : A) (hx : x ∈ s), p x (subset_adjoin R s hx))
(add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy)) (zero : p 0 (zero_mem _))
(mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
(smul : ∀ (r : R) x hx, p x hx → p (r • x) (SMulMemClass.smul_mem r hx))
(star : ∀ x hx, p x hx → p (star x) (star_mem hx)) {a : A} (ha : a ∈ adjoin R s) : p a ha :=
by
refine NonUnitalAlgebra.adjoin_induction (fun x hx ↦ ?_) add zero mul smul ha
simp only [Set.mem_union, Set.mem_star] at hx
obtain (hx | hx) := hx
· exact mem x hx
· simpa using star _ (NonUnitalAlgebra.subset_adjoin R (by simpa using Or.inl hx)) (mem _ hx)
