English
Let {S_i} be a family of subgroups of G indexed by ι. If a property C holds for 1 and for every i for all x ∈ S_i, C x, and C is preserved under multiplication, then C holds for every x ∈ ⨆ i, S_i.
Русский
Пусть {S_i} — семья подпгрупп подгрупп G, индексация по ι. Пусть свойство C выполняется для 1 и для каждого i для всех x ∈ S_i, если C x, и сохраняется при умножении. Тогда C выполняется для каждого элемента ⨆ i, S_i.
LaTeX
$$$\\text{Let } S_i\\subseteq G\\; (i\\in\\iota),\\;\\ C: G\\to\\text{Prop}. \\(x\\in\\langle\\bigcup_i S_i\\rangle\\Rightarrow C(x)\\). \\\\ \\,\\text{Assume } (\\forall i) (\\forall x\\in S_i)\\; C(x) \\\\ \\text{and } C(1),\\; (\\forall x,y)\\; C(x)\\to C(y)\\to C(xy). \\\\ \\text{Then } C(x)\\text{ for all }x\\in \\bigsqcup_i S_i.$$
Lean4
/-- An induction principle for elements of `⨆ i, S i`.
If `C` holds for `1` and all elements of `S i` for all `i`, and is preserved under multiplication,
then it holds for all elements of the supremum of `S`. -/
@[to_additive (attr := elab_as_elim) /-- An induction principle for elements of `⨆ i, S i`.
If `C` holds for `0` and all elements of `S i` for all `i`, and is preserved under addition,
then it holds for all elements of the supremum of `S`. -/
]
theorem iSup_induction {ι : Sort*} (S : ι → Subgroup G) {C : G → Prop} {x : G} (hx : x ∈ ⨆ i, S i)
(mem : ∀ (i), ∀ x ∈ S i, C x) (one : C 1) (mul : ∀ x y, C x → C y → C (x * y)) : C x :=
by
rw [iSup_eq_closure] at hx
induction hx using closure_induction'' with
| one => exact one
| mem x hx =>
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
exact mem _ _ hi
| inv_mem x hx =>
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
exact mem _ _ (inv_mem hi)
| mul x y _ _ ihx ihy => exact mul x y ihx ihy
