English
Let s be a subset of a ring R and p a predicate on R. If p holds for 0 and for all elements of s, and p is preserved under addition, negation, and left and right multiplication, then p holds for all elements of span(s).
Русский
Пусть s ⊆ R и пусть p — предикат на R. Если p выполняется для 0 и для каждого элемента множества s, и если p сохраняется при сложении, отрицании и левой и правой умножении, тогда p выполняется для каждого элемента span(s).
LaTeX
$$$\\forall p:\\\\mathbb{R}\\\\to \\\\text{Prop},\\\\big( p(0) \\\\land \\\\forall x\\\\in s,\ p(x) \\\\,\\\\land\\\\ p \\,\nobreak\\\\(x+y) \\\\land \\\\forall a x,\ p(x) \to p(a x) \\\\land \\\\forall b x,\ p(x) \to p(x b) \\big) \\\\Rightarrow \\\\forall x\\\\in \\\\operatorname{span}(s),\\\\, p(x) $$$
Lean4
/-- An induction principle for span membership.
If `p` holds for 0 and all elements of `s`,
and is preserved under addition and left and right multiplication,
then `p` holds for all elements of the span of `s`. -/
@[elab_as_elim]
theorem span_induction {s : Set R} {p : (x : R) → x ∈ TwoSidedIdeal.span s → Prop}
(mem : ∀ (x) (h : x ∈ s), p x (subset_span h)) (zero : p 0 (zero_mem _))
(add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem _ hx hy)) (neg : ∀ x hx, p x hx → p (-x) (neg_mem _ hx))
(left_absorb : ∀ a x hx, p x hx → p (a * x) (mul_mem_left _ _ _ hx))
(right_absorb : ∀ b x hx, p x hx → p (x * b) (mul_mem_right _ _ _ hx)) {x : R} (hx : x ∈ span s) : p x hx :=
let J : TwoSidedIdeal R :=
.mk' {x | ∃ hx, p x hx} ⟨zero_mem _, zero⟩
(fun ⟨hx1, hx2⟩ ⟨hy1, hy2⟩ ↦ ⟨add_mem _ hx1 hy1, add _ _ hx1 hy1 hx2 hy2⟩)
(fun ⟨hx1, hx2⟩ ↦ ⟨neg_mem _ hx1, neg _ hx1 hx2⟩)
(fun {x' y'} ⟨hy1, hy2⟩ ↦ ⟨mul_mem_left _ _ _ hy1, left_absorb _ _ _ hy2⟩)
(fun {x' y'} ⟨hx1, hx2⟩ ↦ ⟨mul_mem_right _ _ _ hx1, right_absorb _ _ _ hx2⟩)
span_le (s := s) (I := J) |>.2 (fun x hx ↦ ⟨by simpa using (mem_span_iff.2 fun I a ↦ a hx), by simp_all⟩) hx |>.elim
fun _ ↦ by simp
