English
For sets s and t, AEMeasurable on the union is equivalent to being AEMeasurable on each piece: f with μ restricted to s ∪ t is AEMeasurable iff f is AEMeasurable on μ|_s and μ|_t.
Русский
Для подмножеств s и t равносильна AЕ-измеримость на объединении и на каждом из них: AEMeasurable(f, μ|_{s∪t}) эквивалентно AEMeasurable(f, μ|_s) и AEMeasurable(f, μ|_t).
LaTeX
$$$\mathrm{AEMeasurable}(f, \mu\restriction (s \cup t)) \iff \mathrm{AEMeasurable}(f, \mu\restriction s) \land \mathrm{AEMeasurable}(f, \mu\restriction t)$$
Lean4
@[simp]
theorem _root_.aemeasurable_union_iff {s t : Set α} :
AEMeasurable f (μ.restrict (s ∪ t)) ↔ AEMeasurable f (μ.restrict s) ∧ AEMeasurable f (μ.restrict t) := by
simp only [union_eq_iUnion, aemeasurable_iUnion_iff, Bool.forall_bool, cond, and_comm]
