English
If i1,i2 are MeasurableEmbeddings covering the universe via their ranges, then measurability of preimages under i1 and i2 implies measurability of s.
Русский
Если i1 и i2 — измеримые вложения, покрывающие вселенную через свои диапазоны, тогда измеримость предобразов s по i1 и i2 влечёт измеримость s.
LaTeX
$$$$ \text{MeasurableEmbedding } i_1 \to \text{MeasurableEmbedding } i_2 \to (univ \subseteq range(i_1) \cup range(i_2)) \to \text{MeasurableSet}(i_1^{-1} s) \to \text{MeasurableSet}(i_2^{-1} s) \to \text{MeasurableSet}(s). $$$$
Lean4
theorem of_union_range_cover (hi₁ : MeasurableEmbedding i₁) (hi₂ : MeasurableEmbedding i₂)
(h : univ ⊆ range i₁ ∪ range i₂) (hf₁ : Measurable (f ∘ i₁)) (hf₂ : Measurable (f ∘ i₂)) : Measurable f :=
fun _s hs ↦ .of_union_range_cover hi₁ hi₂ h (hf₁ hs) (hf₂ hs)
