English
Same as 1515: the induction principle for adjoin.
Русский
То же, что и 1515: индукция для адъюнкта.
LaTeX
$$Same as 1515$$
Lean4
@[elab_as_elim]
theorem adjoin_induction {p : (x : A) → x ∈ adjoin R s → Prop} (mem : ∀ (x) (hx : x ∈ s), p x (subset_adjoin hx))
(algebraMap : ∀ r, p (algebraMap R A r) (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)) {x : A} (hx : x ∈ adjoin R s) : p x hx :=
let S : Subalgebra R A :=
{ carrier := {x | ∃ hx, p x hx}
mul_mem' := by rintro _ _ ⟨_, hpx⟩ ⟨_, hpy⟩; exact ⟨_, mul _ _ _ _ hpx hpy⟩
add_mem' := by rintro _ _ ⟨_, hpx⟩ ⟨_, hpy⟩; exact ⟨_, add _ _ _ _ hpx hpy⟩
algebraMap_mem' := fun r ↦ ⟨_, algebraMap r⟩ }
adjoin_le (S := S) (fun y hy ↦ ⟨subset_adjoin hy, mem y hy⟩) hx |>.elim fun _ ↦ _root_.id
