English
If i1,i2,i3 are MeasurableEmbeddings with univ ⊆ range i1 ∪ range i2 ∪ range i3, and the preimages i1⁻¹'(s), i2⁻¹'(s), i3⁻¹'(s) are measurable, then s is measurable.
Русский
Пусть i1,i2,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₃) (hf₁ : Measurable (f ∘ i₁))
(hf₂ : Measurable (f ∘ i₂)) (hf₃ : Measurable (f ∘ i₃)) : Measurable f := fun _s hs ↦
.of_union₃_range_cover hi₁ hi₂ hi₃ h (hf₁ hs) (hf₂ hs) (hf₃ hs)
