English
An induction principle for elements of ⨆ i, p_i: if a property holds for 0 and each p_i element, and is preserved under addition, then it holds for all elements of the supremum.
Русский
Индукционное свойство по элементам ⨆ i, p_i: если свойство верно для 0 и для каждого элемента p_i, и сохраняется под сложение, то оно верно для любого элемента ⨆ i, p_i.
LaTeX
$$$$ \\text{motive}(x) \\quad \\text{whenever} \\quad x \\in \\bigvee_i p_i, $$$$
Lean4
/-- An induction principle for elements of `⨆ i, p i`.
If `C` holds for `0` and all elements of `p i` for all `i`, and is preserved under addition,
then it holds for all elements of the supremum of `p`. -/
@[elab_as_elim]
theorem iSup_induction {ι : Sort*} (p : ι → Submodule R M) {motive : M → Prop} {x : M} (hx : x ∈ ⨆ i, p i)
(mem : ∀ (i), ∀ x ∈ p i, motive x) (zero : motive 0) (add : ∀ x y, motive x → motive y → motive (x + y)) :
motive x := by
rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx
exact AddSubmonoid.iSup_induction (x := x) _ hx mem zero add
