English
If a predicate holds for all generators and is closed under algebraic operations, then it holds for all elements of adjoin R s.
Русский
Если предикат выполняется для всех образующих и замкнут относительно операций алгебры, тогда он выполняется для всех элементов adjoin R s.
LaTeX
$$$\text{adjoin}_R(s)\text{ induction: } p\;x\;{x \in \operatorname{adjoin}_R(s)}$$$
Lean4
/-- If some predicate holds for all `x ∈ (s : Set A)` and this predicate is closed under the
`algebraMap`, addition, multiplication and star operations, then it holds for `a ∈ adjoin R s`. -/
@[elab_as_elim]
theorem adjoin_induction {s : Set A} {p : (x : A) → x ∈ adjoin R s → Prop}
(mem : ∀ (x) (hx : x ∈ s), p x (subset_adjoin R 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 x hx, p x hx → p (r • x) (SMulMemClass.smul_mem r hx)) {x} (hx : x ∈ adjoin R s) : p x hx :=
let S : NonUnitalSubalgebra R A :=
{ carrier := {x | ∃ hx, p x hx}
mul_mem' := (Exists.elim · fun _ ha ↦ (Exists.elim · fun _ hb ↦ ⟨_, mul _ _ _ _ ha hb⟩))
add_mem' := (Exists.elim · fun _ ha ↦ (Exists.elim · fun _ hb ↦ ⟨_, add _ _ _ _ ha hb⟩))
smul_mem' := fun r ↦ (Exists.elim · fun _ hb ↦ ⟨_, smul r _ _ hb⟩)
zero_mem' := ⟨_, zero⟩ }
adjoin_le (S := S) (fun y hy ↦ ⟨subset_adjoin R hy, mem y hy⟩) hx |>.elim fun _ ↦ id
