English
Let i1, i2, i3 be MeasurableEmbeddings with univ ⊆ range i1 ∪ range i2 ∪ range i3, and suppose MeasurableSets for i1⁻¹'(s), i2⁻¹'(s), i3⁻¹'(s). Then s is measurable.
Русский
Пусть i1, i2, i3 — измеримые вложения с покрытием univ ⊆ range i1 ∪ range i2 ∪ range i3. Если i1⁻¹'(s), i2⁻¹'(s) и i3⁻¹'(s) измеримы, то s измеримо.
LaTeX
$$$$ \text{MeasurableEmbedding } i_1 \to \text{MeasurableEmbedding } i_2 \to \text{MeasurableEmbedding } i_3 \to (univ \subseteq range(i_1) \cup range(i_2) \cup range(i_3)) \to \text{MeasurableSet}(i_1^{-1} s) \to \text{MeasurableSet}(i_2^{-1} s) \to \text{MeasurableSet}(i_3^{-1} s) \to \text{MeasurableSet}(s). $$$$
Lean4
theorem of_union₃_range_cover (hi₁ : MeasurableEmbedding i₁) (hi₂ : MeasurableEmbedding i₂)
(hi₃ : MeasurableEmbedding i₃) (h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃) (hs₁ : MeasurableSet (i₁ ⁻¹' s))
(hs₂ : MeasurableSet (i₂ ⁻¹' s)) (hs₃ : MeasurableSet (i₃ ⁻¹' s)) : MeasurableSet s :=
by
convert (hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂) |>.union (hi₃.measurableSet_image' hs₃)
simp [image_preimage_eq_range_inter, ← union_inter_distrib_right, univ_subset_iff.1 h]
