English
If s is dense in M, i.e., closure(s) = ⊤, then to prove a predicate p holds for all x ∈ M it suffices to verify p for x ∈ s and that p is preserved under multiplication.
Русский
Если s плотна в M, то чтобы доказать, что предикат p верен для всех элементов M, достаточно проверить p на x в s и что p сохраняется при умножении.
LaTeX
$$$p:\\; M \\to \\mathrm{Prop},\\; closure(s)=\\top,\\; (\\forall x\\in s,\\; p(x)) \\land (\\forall x,y,\\; p(x) \\to p(y) \\to p(xy)) \\Rightarrow \\forall x,\\; p(x)$$$
Lean4
/-- If `s` is a dense set in a magma `M`, `Subsemigroup.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`,
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`,
`AddSubsemigroup.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`, and verify that `p x` and `p y` imply
`p (x + y)`. -/
]
theorem dense_induction {p : M → Prop} (s : Set M) (closure : closure s = ⊤) (mem : ∀ x ∈ s, p x)
(mul : ∀ x y, p x → p y → p (x * y)) (x : M) : p x := by
induction closure.symm ▸ mem_top x using closure_induction with
| mem _ h => exact mem _ h
| mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
