English
Adjoin induction provides an eliminator: if a property holds for generators s, is preserved by algebra maps, addition and multiplication, then it holds for all elements of adjoin R s.
Русский
Индукция Adjoin обеспечивает элементарный вывод: если свойство верно для образующих s и сохраняется под алгебраическими отображениями, сложением и умножением, то оно верно для всего элемента adjoin R s.
LaTeX
$$$\\text{adjoin\_induction} \\,:\\; \\forall p :(x\\in \\operatorname{adjoin} R s)\\to Prop,\\; (\\forall x\\in s, p(x,\\subset\_adjoin)) \\land (\\forall r, p({\\mathrm algebraMap}(R,A) r)) \\land \\cdots \\Rightarrow \\forall x\\in \\operatorname{adjoin} R s, p(x)$$$
Lean4
theorem adjoin_eq (S : Subalgebra R A) : adjoin R ↑S = S :=
adjoin_eq_of_le _ (Set.Subset.refl _) subset_adjoin
