English
The closure of a set equals the union of {1} and the closure generated by the set’s elements (viewed as a subsemigroup).
Русский
Замыкание набора равно объединению {1} и замыкания, порождаемого этим набором как полусубгруппы.
LaTeX
$$closure s = {1} ∪ (Subsemigroup.closure s)$$
Lean4
/-- If `s` is a dense set in a monoid `M`, `Submonoid.closure s = ⊤`, then in order to prove that
some predicate `p` holds for all `x : M` it suffices to verify `p x` for `x ∈ s`, verify `p 1`,
and verify that `p x` and `p y` imply `p (x * y)`. -/
@[to_additive (attr := elab_as_elim) /--
If `s` is a dense set in an additive monoid `M`, `AddSubmonoid.closure s = ⊤`, then in
order to prove that some predicate `p` holds for all `x : M` it suffices to verify `p x` for
`x ∈ s`, verify `p 0`, and verify that `p x` and `p y` imply `p (x + y)`. -/
]
theorem dense_induction {motive : M → Prop} (s : Set M) (closure : closure s = ⊤) (mem : ∀ x ∈ s, motive x)
(one : motive 1) (mul : ∀ x y, motive x → motive y → motive (x * y)) (x : M) : motive x := by
induction closure.symm ▸ mem_top x using closure_induction with
| mem _ h => exact mem _ h
| one => exact one
| mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
