English
If a predicate p holds on a family C of sets, is preserved under empty, complement, and countable unions, and is closed under unions of sequences, then p holds for all sets measurable in generateFrom C.
Русский
Если свойство p верно на наборе C множеств и сохраняется при пустом множестве, дополнении и счетных объединениях, а также замыкается на объединениях последовательностей, то p верно для всех измеримых множеств в generateFrom C.
LaTeX
$$$\\forall C\\subseteq\\mathcal{P}(\\alpha),\\; p\\text{ satisfies the four closure conditions} \\Rightarrow \\forall s\\; (s\\ \ntext{MeasurableSet}[\\text{generateFrom}(C)]\\ s)$$$
Lean4
@[elab_as_elim]
theorem generateFrom_induction (C : Set (Set α)) (p : ∀ s : Set α, MeasurableSet[generateFrom C] s → Prop)
(hC : ∀ t ∈ C, ∀ ht, p t ht) (empty : p ∅ (measurableSet_empty _)) (compl : ∀ t ht, p t ht → p tᶜ ht.compl)
(iUnion :
∀ (s : ℕ → Set α) (hs : ∀ n, MeasurableSet[generateFrom C] (s n)),
(∀ n, p (s n) (hs n)) → p (⋃ i, s i) (.iUnion hs))
(s : Set α) (hs : MeasurableSet[generateFrom C] s) : p s hs :=
by
induction hs
exacts [hC _ ‹_› _, empty, compl _ ‹_› ‹_›, iUnion ‹_› ‹_› ‹_›]
