English
If x lies in the supremum of a family N_i, and a predicate motive is closed under zero and closed under addition, and preserved by each N_i, then motive holds for x.
Русский
Если x принадлежит суперобъединению семейства N_i и свойство motive удовлетворяет условиям нуля и замыкания на сложение и сохраняется на каждом N_i, то motive выполняется для x.
LaTeX
$$$x \in \bigvee_i N_i \quad\Rightarrow\quad (\forall i,\; y \in N_i \Rightarrow motive(y)) \;\land\; motive(0) \land (\forall y,z, motive(y) \land motive(z) \Rightarrow motive(y+z)) \Rightarrow motive(x)$$$
Lean4
@[elab_as_elim]
theorem iSup_induction {ι} (N : ι → LieSubmodule R L M) {motive : M → Prop} {x : M} (hx : x ∈ ⨆ i, N i)
(mem : ∀ i, ∀ y ∈ N i, motive y) (zero : motive 0) (add : ∀ y z, motive y → motive z → motive (y + z)) : motive x :=
by
rw [← LieSubmodule.mem_toSubmodule, LieSubmodule.iSup_toSubmodule] at hx
exact Submodule.iSup_induction (motive := motive) (fun i ↦ (N i : Submodule R M)) hx mem zero add
