English
A dependent induction principle on ⨆ i, p_i: for a motive that depends on x and hx, if it holds for each i and hx, for 0 and additive closure it holds for all x in the supremum.
Русский
Зависимое индукционное принцип на ⨆ i, p_i: если свойство зависит от x и hx, верно для каждого i и hx, для 0 и сложения — верно для всех x в ⨆ i, p_i.
LaTeX
$$$$ \\text{motive}(x, hx) $$ with the dependent induction rules$$
Lean4
/-- A dependent version of `submodule.iSup_induction`. -/
@[elab_as_elim]
theorem iSup_induction' {ι : Sort*} (p : ι → Submodule R M) {motive : ∀ x, (x ∈ ⨆ i, p i) → Prop}
(mem : ∀ (i) (x) (hx : x ∈ p i), motive x (mem_iSup_of_mem i hx)) (zero : motive 0 (zero_mem _))
(add : ∀ x y hx hy, motive x hx → motive y hy → motive (x + y) (add_mem ‹_› ‹_›)) {x : M} (hx : x ∈ ⨆ i, p i) :
motive x hx := by
refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, p i) (hc : motive x hx) => hc
refine
iSup_induction p (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), motive x hx) hx (fun i x hx => ?_) ?_ fun x y => ?_
· exact ⟨_, mem _ _ hx⟩
· exact ⟨_, zero⟩
· rintro ⟨_, Cx⟩ ⟨_, Cy⟩
exact ⟨_, add _ _ _ _ Cx Cy⟩
