English
A dependent version of iSup_induction allowing motive to depend on the element x and the membership proof.
Русский
Зависимая версия iSup_induction, допускающая зависимость свойства от элемента x и доказательства принадлежности.
LaTeX
$$iSup_induction'(S, motive, mem) : motive x mem$$
Lean4
/-- A dependent version of `Subalgebra.iSup_induction`. -/
@[elab_as_elim]
theorem iSup_induction' {ι : Sort*} (S : ι → Subalgebra R A) {motive : ∀ x, (x ∈ ⨆ i, S i) → Prop} {x : A}
(mem : x ∈ ⨆ i, S i) (basic : ∀ (i) (x) (hx : x ∈ S i), motive x (mem_iSup_of_mem i hx))
(zero : motive 0 (zero_mem _)) (one : motive 1 (one_mem _))
(add : ∀ x y hx hy, motive x hx → motive y hy → motive (x + y) (add_mem ‹_› ‹_›))
(mul : ∀ x y hx hy, motive x hx → motive y hy → motive (x * y) (mul_mem ‹_› ‹_›))
(algebraMap : ∀ r, motive (algebraMap R A r) (Subalgebra.algebraMap_mem _ ‹_›)) : motive x mem :=
by
refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) ↦ hc
exact
iSup_induction S (motive := fun x' ↦ ∃ h, motive x' h) mem (fun _ _ h ↦ ⟨_, basic _ _ h⟩) ⟨_, zero⟩ ⟨_, one⟩
(fun _ _ h h' ↦ ⟨_, add _ _ _ _ h.2 h'.2⟩) (fun _ _ h h' ↦ ⟨_, mul _ _ _ _ h.2 h'.2⟩) fun _ ↦ ⟨_, algebraMap _⟩
