English
Let S be a family of subsemigroups; if a property C holds for all elements of every S(i) and is closed under multiplication, then C holds for every element of the supremum ⨆ i, S i.
Русский
Пусть S—семейство подполугрупп; если свойство C выполняется для всех элементов каждого S(i) и замкнуто относительно умножения, тогда C выполняется для каждого элемента верхнего предела ⨆ i, S i.
LaTeX
$$$\\bigl( x_1 \\in \\bigsqcup_i S(i) \\bigr) \\Rightarrow \\Bigl( \\bigl( \\forall i, \\forall x_2 \\in S(i), C(x_2) \\bigr) \\land \\bigl( \\forall x,y, C(x) \\rightarrow C(y) \\rightarrow C(xy) \\bigr) \\rightarrow C(x_1) \\Bigr)$$$
Lean4
/-- An induction principle for elements of `⨆ i, S i`.
If `C` holds 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 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 (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i)
(mem : ∀ i, ∀ x₂ ∈ S i, C x₂) (mul : ∀ x y, C x → C y → C (x * y)) : C x₁ :=
by
rw [iSup_eq_closure] at hx₁
refine closure_induction (fun x₂ hx₂ => ?_) (fun x y _ _ ↦ mul x y) hx₁
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx₂
exact mem _ _ hi
