English
An induction principle: if a property p holds for every open retrocompact set and is closed under union and complement, then p holds for all constructible sets.
Русский
Принцип индукции по конструируемым множествам: если свойство p выполняется для всех открытых ретрокомпактных множеств и сохраняется при объединении и дополнении, то оно выполняется для всех конструируемых множеств.
LaTeX
$$$\\forall p:\\nobrace{\\forall s\\ setmember X, IsConstructible(s) \\Rightarrow Prop}{},\\;\\Bigl(\\forall U\\, (hUopen: IsOpen(U))\\,(hUcomp: IsRetrocompact(U)), p(U, \\text{subset\_closure}(\\langle hUopen, hUcomp \\rangle))\\Bigr) \\\\land \\\\Bigl(\\forall s\\, hs\\, t\\, ht, p(s, hs) \\Rightarrow p(t, ht) \\Rightarrow p(s \\cup t, hs.union ht)\\Bigr) \\\\land \\\\Bigl(\\forall s\\, hs, p(s, hs) \\Rightarrow p(s^c, hs.compl)\\Bigr) \\\\Rightarrow \\\\forall {s}, IsConstructible(s) \\Rightarrow p(s, IsConstructible(s)).$$$
Lean4
/-- An induction principle for constructible sets. If `p` holds for all open retrocompact
sets, and is preserved under union and complement, then `p` holds for all constructible sets. -/
@[elab_as_elim]
theorem empty_union_induction {p : ∀ s : Set X, IsConstructible s → Prop}
(open_retrocompact :
∀ U (hUopen : IsOpen U) (hUcomp : IsRetrocompact U), p U (BooleanSubalgebra.subset_closure ⟨hUopen, hUcomp⟩))
(union : ∀ s hs t ht, p s hs → p t ht → p (s ∪ t) (hs.union ht)) (compl : ∀ s hs, p s hs → p sᶜ hs.compl) {s}
(hs : IsConstructible s) : p s hs := by
induction hs using BooleanSubalgebra.closure_bot_sup_induction with
| mem U hU => exact open_retrocompact _ hU.1 hU.2
| bot => exact open_retrocompact _ isOpen_empty .empty
| sup s hs t ht hs' ht' => exact union _ _ _ _ hs' ht'
| compl s hs hs' => exact compl _ _ hs'
