English
If s is Lindelöf and p is stable under union and restriction with a local witness near each x∈s, then p(s) holds.
Русский
Если s — Линдельёфово множество, и p сохраняется под объединением и ограничением, и у каждого x∈s есть локальное доказательство, то p(s) выполняется.
LaTeX
$$$$\text{IsLindelof}(s) \Rightarrow (p\text{ invariant under } \cup,\cap s) \Rightarrow p(s).$$$$
Lean4
/-- If `p : Set X → Prop` is stable under restriction and union, and each point `x`
of a Lindelöf set `s` has a neighborhood `t` within `s` such that `p t`, then `p s` holds. -/
@[elab_as_elim]
theorem induction_on (hs : IsLindelof s) {p : Set X → Prop} (hmono : ∀ ⦃s t⦄, s ⊆ t → p t → p s)
(hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S))
(hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t) : p s :=
by
let f : Filter X := ofCountableUnion p hcountable_union (fun t ht _ hsub ↦ hmono hsub ht)
have : sᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa [f] using hnhds)
rwa [← compl_compl s]
