English
A dependent version of iSup_induction: if a dependent motive holds for each i and each x ∈ S_i, then it holds for all x in ⨆ i, S_i.
Русский
Зависимый вариант iSup_induction: если зависимое свойство выполняется для каждого i и каждого x ∈ S_i, то оно выполняется для всех x в ⨆ i, S_i.
LaTeX
$$$\forall i, ∀ x ∈ S_i,\ motive\ x\, hx \Rightarrow \forall x, x ∈ ⨆ i, S_i \Rightarrow \text{motive } x hx$$$
Lean4
/-- A dependent version of `Submonoid.iSup_induction`. -/
@[to_additive (attr := elab_as_elim) /-- A dependent version of `AddSubmonoid.iSup_induction`. -/
]
theorem iSup_induction' {ι : Sort*} (S : ι → Submonoid M) {motive : ∀ x, (x ∈ ⨆ i, S i) → Prop}
(mem : ∀ (i), ∀ (x) (hxS : x ∈ S i), motive x (mem_iSup_of_mem i hxS)) (one : motive 1 (one_mem _))
(mul : ∀ x y hx hy, motive x hx → motive y hy → motive (x * y) (mul_mem ‹_› ‹_›)) {x : M} (hx : x ∈ ⨆ i, S i) :
motive x hx :=
by
refine Exists.elim (?_ : ∃ Hx, motive x Hx) fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) => hc
refine @iSup_induction _ _ ι S (fun m => ∃ hm, motive m hm) _ hx (fun i x hx => ?_) ?_ fun x y => ?_
· exact ⟨_, mem _ _ hx⟩
· exact ⟨_, one⟩
· rintro ⟨_, Cx⟩ ⟨_, Cy⟩
exact ⟨_, mul _ _ _ _ Cx Cy⟩
