English
Let s be a set. For any predicate P on pairs (x,y) with x,y ∈ adjoin R s, if P holds under the base operations (membership from s, algebra maps, addition, multiplication, star), then P holds for all pairs in adjoin R s.
Русский
Пусть s — множество. Для пары (x,y) с x,y ∈ adjoin R s, если свойство сохраняется под включениями, алгебраическими отображениями и операциями, то оно верно и для всех пар внутри adjoin R s.
LaTeX
$$$\forall a,b \in \mathrm{adjoin}(R,s),\; P(a,b) \text{ holds if base, algebraMap, add, mul, star closures hold.}$$$
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) (h : x ∈ s), p x (subset_adjoin R s h))
(algebraMap : ∀ r, p (_root_.algebraMap R _ r) (_root_.algebraMap_mem _ r))
(add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy))
(mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) (star : ∀ x hx, p x hx → p (star x) (star_mem hx))
{a : A} (ha : a ∈ adjoin R s) : p a ha :=
by
refine Algebra.adjoin_induction (fun x hx ↦ ?_) algebraMap add mul ha
simp only [Set.mem_union, Set.mem_star] at hx
obtain (hx | hx) := hx
· exact mem x hx
· simpa using star _ (Algebra.subset_adjoin (by simpa using Or.inl hx)) (mem _ hx)
