English
If a closed property holds on a dense subset s, it holds for all of X.
Русский
Если свойство P имеет замкнутое множество точек и выполняется на плотной подмножестве s, то оно выполняется на всем X.
LaTeX
$$$\operatorname{Dense}(s) \rightarrow (\forall x \in s, P(x)) \rightarrow \mathrm{IsClosed}\{x : X \mid P(x)\} \rightarrow \forall x, P(x)$$$
Lean4
/-- If a closed property holds for a dense subset, it holds for the whole space. -/
@[elab_as_elim]
theorem induction (hs : Dense s) {P : X → Prop} (mem : ∀ x ∈ s, P x) (isClosed : IsClosed {x | P x}) (x : X) : P x :=
hs.closure_eq.symm.subset.trans (isClosed.closure_subset_iff.mpr mem) (Set.mem_univ _)
