English
An AE version of induction on a generating family of sets: if a predicate C(x,t) is satisfied for ∅ and for all t in a generating π-system, and is closed under complement and countable disjoint unions, then for a.e. x, C(x,t) holds for all measurable t.
Русский
AE-версия индукции по порождению σ-алгебры: если предикат C(x,t) выполняется для пустого множества и для всех t из порождающей π-системы, а также древируется замкнутым по дополнениям и счётным попарно непересекающимся объединениям, то для почти всех x выполняется C(x,t) для всех измеримых t.
LaTeX
$$⟨AE версия индукции на пересечениях: при заданных условиях на семейство S и предикат C(x,t), ∀ᵐ x ∂μ, ∀ t Measurable, C(x,t)⟩$$
Lean4
/-- Given a predicate on `β` and `Set α` where both `α` and `β` are measurable spaces, if the
predicate holds for almost every `x : β` and
- `∅ : Set α`
- a family of sets generating the σ-algebra of `α`
Moreover, if for almost every `x : β`, the predicate is closed under complements and countable
disjoint unions, then the predicate holds for almost every `x : β` and all measurable sets of `α`.
This is an AE version of `MeasurableSpace.induction_on_inter` where the condition is dependent
on a measurable space `β`. -/
theorem _root_.MeasurableSpace.ae_induction_on_inter {α β : Type*} [MeasurableSpace β] {μ : Measure β}
{C : β → Set α → Prop} {s : Set (Set α)} [m : MeasurableSpace α] (h_eq : m = MeasurableSpace.generateFrom s)
(h_inter : IsPiSystem s) (h_empty : ∀ᵐ x ∂μ, C x ∅) (h_basic : ∀ᵐ x ∂μ, ∀ t ∈ s, C x t)
(h_compl : ∀ᵐ x ∂μ, ∀ t, MeasurableSet t → C x t → C x tᶜ)
(h_union :
∀ᵐ x ∂μ,
∀ f : ℕ → Set α, Pairwise (Disjoint on f) → (∀ i, MeasurableSet (f i)) → (∀ i, C x (f i)) → C x (⋃ i, f i)) :
∀ᵐ x ∂μ, ∀ ⦃t⦄, MeasurableSet t → C x t := by
filter_upwards [h_empty, h_basic, h_compl, h_union] with x hx_empty hx_basic hx_compl hx_union using
MeasurableSpace.induction_on_inter (C := fun t _ ↦ C x t) h_eq h_inter hx_empty hx_basic hx_compl hx_union
