English
If the closure of s is top (dense), then to prove a property p for a fixed x ∈ M it suffices to show p on s and that p is preserved under all function symbols.
Русский
Если замыкание s равно ⊤ (сильно плотно), то чтобы доказать свойство p для заданного x ∈ M, достаточно проверить p на s и то, что p сохраняется под всеми функциями языка.
LaTeX
$$$$ \operatorname{closure}_L(s) = \top \implies (\forall x \in s, p(x)) \land (\forall n, \forall f, \operatorname{ClosedUnder}(f, \{x : p(x)\})) \Rightarrow p(x). $$$$
Lean4
/-- If `s` is a dense set in a structure `M`, `Substructure.closure L 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` is preserved under function symbols. -/
@[elab_as_elim]
theorem dense_induction {p : M → Prop} (x : M) {s : Set M} (hs : closure L s = ⊤) (Hs : ∀ x ∈ s, p x)
(Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)) : p x :=
by
have : ∀ x ∈ closure L s, p x := fun x hx => closure_induction hx Hs fun {n} => Hfun
simpa [hs] using this x
