English
Let S_i be subgroups of G indexed by ι and C a predicate on pairs (x,h) where h asserts x ∈ ⨆ i, S_i. If hp(i,x,hx) holds for all i and x ∈ S_i, h1 asserts C(1,(one_mem _)), and hmux ensures closure under multiplication, then C holds for all x with hx ∈ ⨆ i, S_i.
Русский
Пусть S_i — подпгруппы G, индексированные по ι, а C — предикат на пары (x,h), где h утверждает x ∈ ⨆ i, S_i. Если выполняются условия hp, h1 и hmux, то C верно для всех x с hx ∈ ⨆ i, S_i.
LaTeX
$$$\\text{Let } S_i\\subseteq G\\ (i\\in\\iota),\\ C:\\forall x, (x\\in\\langle S_i\\rangle)\\to\\mathrm{Prop}. \\\\ hp(i,x,hx): x\\in S_i \\Rightarrow C(x,\\,mem\\_iSup\_of\_mem\\ i\\ hx). \\\\ h1: C(1,(one\\_mem _)). \\\\ hmul: \\forall x y hx hy, C x hx \\to C y hy \\to C(xy, mul\\_mem hx hy). \\\\ \\forall {x} (hx): C x hx.$$
Lean4
/-- A dependent version of `Subgroup.iSup_induction`. -/
@[to_additive (attr := elab_as_elim) /-- A dependent version of `AddSubgroup.iSup_induction`. -/
]
theorem iSup_induction' {ι : Sort*} (S : ι → Subgroup G) {C : ∀ x, (x ∈ ⨆ i, S i) → Prop}
(hp : ∀ (i), ∀ x (hx : x ∈ S i), C x (mem_iSup_of_mem i hx)) (h1 : C 1 (one_mem _))
(hmul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›)) {x : G} (hx : x ∈ ⨆ i, S i) : C x hx :=
by
suffices ∃ h, C x h from this.snd
refine iSup_induction S (C := fun x => ∃ h, C x h) hx (fun i x hx => ?_) ?_ fun x y => ?_
· exact ⟨_, hp i _ hx⟩
· exact ⟨_, h1⟩
· rintro ⟨_, Cx⟩ ⟨_, Cy⟩
exact ⟨_, hmul _ _ _ _ Cx Cy⟩
