English
A two-argument induction principle for adjoin: if a predicate on pairs (x,y) is preserved under the star-closure operations and the algebraic operations, then it holds for all pairs in adjoin.
Русский
Две переменные индукции для пары: если свойство сохраняется под все операции, то оно выполняется на всех парах внутри adjoin.
LaTeX
$$$\\text{adjoin\_induction\_2} (s, P, \\ldots) : \\forall a,b\\in \\mathrm{adjoin}(R,s), P(a,b).$$$
Lean4
@[elab_as_elim]
theorem adjoin_induction₂ {s : Set A} {p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop}
(mem_mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), p x y (subset_adjoin R s hx) (subset_adjoin R s hy))
(algebraMap_both :
∀ r₁ r₂, p (algebraMap R A r₁) (algebraMap R A r₂) (_root_.algebraMap_mem _ r₁) (_root_.algebraMap_mem _ r₂))
(algebraMap_left :
∀ (r) (x) (hx : x ∈ s), p (algebraMap R A r) x (_root_.algebraMap_mem _ r) (subset_adjoin R s hx))
(algebraMap_right :
∀ (r) (x) (hx : x ∈ s), p x (algebraMap R A r) (subset_adjoin R s hx) (_root_.algebraMap_mem _ r))
(add_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x + y) z (add_mem hx hy) hz)
(add_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y + z) hx (add_mem hy hz))
(mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
(mul_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz))
(star_left : ∀ x y hx hy, p x y hx hy → p (star x) y (star_mem hx) hy)
(star_right : ∀ x y hx hy, p x y hx hy → p x (star y) hx (star_mem hy)) {a b : A} (ha : a ∈ adjoin R s)
(hb : b ∈ adjoin R s) : p a b ha hb := by
induction hb using adjoin_induction with
| mem z hz =>
induction ha using adjoin_induction with
| mem _ h => exact mem_mem _ _ h hz
| algebraMap _ => exact algebraMap_left _ _ hz
| mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
| add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
| star _ _ h => exact star_left _ _ _ _ h
| algebraMap r =>
induction ha using adjoin_induction with
| mem _ h => exact algebraMap_right _ _ h
| algebraMap _ => exact algebraMap_both _ _
| mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
| add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
| star _ _ h => exact star_left _ _ _ _ h
| mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
| add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
| star _ _ h => exact star_right _ _ _ _ h
