English
An induction principle for elements of ⨆ i, S_i: if a motive holds for 1 and is closed under multiplication by elements of the S_i, then it holds for every element of the supremum.
Русский
Индуктивный принцип по элементам ⨆ i, S_i: если свойство верно для 1 и сохраняется при умножении на элементы S_i, то оно верно для всех элементов верхней границы.
LaTeX
$$$\text{If } x \in ⨆ i, S_i,\ for\ all\ i,\ if\ m_i\in S_i,\ motive(m_i)\, and\ motive(1),\ motive(x)\Rightarrow motive(x)$$$
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 : ι → Submonoid M) {motive : M → Prop} {x : M} (hx : x ∈ ⨆ i, S i)
(mem : ∀ (i), ∀ x ∈ S i, motive x) (one : motive 1) (mul : ∀ x y, motive x → motive y → motive (x * y)) :
motive x := by
rw [iSup_eq_closure] at hx
refine closure_induction (fun x hx => ?_) one (fun _ _ _ _ ↦ mul _ _) hx
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
exact mem _ _ hi
