English
Let s be a compact subset of a topological space X and let p be a property of subsets of X which is stable under restriction and under unions. If p holds for the empty set, p is monotone with respect to inclusion (s ⊆ t and p(t) implies p(s)), p is closed under unions (p(s) and p(t) imply p(s ∪ t)), and for every x ∈ s there exists a neighborhood t within s with p(t), then p(s) holds.
Русский
Пусть s — компактное подмножество пространства X и пусть p — свойство подмножеств X, устойчивое к ограничению и объединениям. Пусть p(∅) верно, если s ⊆ t и p(t) тогда p(s) (монотонность по включению), p сохраняется при объединении (p(s) и p(t) ⇒ p(s ∪ t)), и для каждого x ∈ s существует окрестность t внутри s такая, что p(t). Тогда p(s) верно.
LaTeX
$$$IsCompact(s) \rightarrow p(\emptyset) \land (\forall \{s t\}, s \subseteq t \rightarrow p(t) \rightarrow p(s)) \land (\forall \{s t\}, p(s) \rightarrow p(t) \rightarrow p(s \cup t)) \land (\forall x \in s, \exists t \in \mathcal{N}[s] x, p(t)) \rightarrow p(s)$$$
Lean4
/-- If `p : Set X → Prop` is stable under restriction and union, and each point `x`
of a compact set `s` has a neighborhood `t` within `s` such that `p t`, then `p s` holds. -/
@[elab_as_elim]
theorem induction_on (hs : IsCompact s) {p : Set X → Prop} (he : p ∅) (hmono : ∀ ⦃s t⦄, s ⊆ t → p t → p s)
(hunion : ∀ ⦃s t⦄, p s → p t → p (s ∪ t)) (hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t) : p s :=
by
let f : Filter X := comk p he (fun _t ht _s hsub ↦ hmono hsub ht) (fun _s hs _t ht ↦ hunion hs ht)
have : sᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa [f] using hnhds)
rwa [← compl_compl s]
