English
Induction principle for measurable sets: if m equals generateFrom(s) and s is a Pi-system, and a predicate C on measurable sets holds for ∅, for every t ∈ s, is closed under complement, and is preserved under countable unions of pairwise disjoint measurable sets, then C holds for all measurable sets.
Русский
Принцип индукции по измеримым множествам: если m = generateFrom(s) и s — π-система, и предикат C на измеримых множествах выполняется для ∅, для каждого t∈s, замыкается по дополнению и сохраняется при объединении попарно непересекающихся счётных семейств, то C выполняется для всех измеримых множеств.
LaTeX
$$$ \text{InductionOnInter: }\; (m=g e n e r a t eFrom(s)) \land IsPiSystem(s) \rightarrow (C(\emptyset) \land (\forall t\in s, C(t)) \land (\forall t, \text{MeasurableSet}(t) \Rightarrow C(t^c)) \land (\forall f: \mathbb{N} \to \Set\alpha, \text{PairwiseDisjoint}(f) \Rightarrow (\forall i, C(f(i)) ) \Rightarrow C(\bigcup_i f(i))) \Rightarrow \forall t, \text{MeasurableSet}(t) \Rightarrow C(t). $$$
Lean4
/-- Induction principle for measurable sets.
If `s` is a π-system that generates the product `σ`-algebra on `α`
and a predicate `C` defined on measurable sets is true
- on the empty set;
- on each set `t ∈ s`;
- on the complement of a measurable set that satisfies `C`;
- on the union of a sequence of pairwise disjoint measurable sets that satisfy `C`,
then it is true on all measurable sets in `α`. -/
@[elab_as_elim]
theorem induction_on_inter {m : MeasurableSpace α} {C : ∀ s : Set α, MeasurableSet s → Prop} {s : Set (Set α)}
(h_eq : m = generateFrom s) (h_inter : IsPiSystem s) (empty : C ∅ .empty)
(basic : ∀ t (ht : t ∈ s), C t <| h_eq ▸ .basic t ht)
(compl : ∀ t (htm : MeasurableSet t), C t htm → C tᶜ htm.compl)
(iUnion :
∀ (f : ℕ → Set α),
Pairwise (Disjoint on f) →
∀ (hfm : ∀ i, MeasurableSet (f i)), (∀ i, C (f i) (hfm i)) → C (⋃ i, f i) (.iUnion hfm)) :
∀ t (ht : MeasurableSet t), C t ht :=
by
have eq : MeasurableSet = DynkinSystem.GenerateHas s :=
by
rw [h_eq, DynkinSystem.generateFrom_eq h_inter]
rfl
suffices ∀ t (ht : DynkinSystem.GenerateHas s t), C t (eq ▸ ht) from fun t ht ↦ this t (eq ▸ ht)
intro t ht
induction ht with
| basic u hu => exact basic u hu
| empty => exact empty
| @compl u hu ihu => exact compl _ (eq ▸ hu) ihu
| @iUnion f hfd hf ihf => exact iUnion f hfd (eq ▸ hf) ihf
