English
Let i1: α1 → α and i2: α2 → α be MeasurableEmbeddings, and suppose univ ⊆ range i1 ∪ range i2. If i1⁻¹'(s) and i2⁻¹'(s) are measurable, then s is measurable.
Русский
Пусть i1: α1 → α и i2: α2 → α — измеримые вложения, и пусть единичное множество покрывается диапазонами: univ ⊆ range i1 ∪ range i2. Если i1⁻¹'(s) и i2⁻¹'(s) измеримы, тогда 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₂) (hs₁ : MeasurableSet (i₁ ⁻¹' s)) (hs₂ : MeasurableSet (i₂ ⁻¹' s)) :
MeasurableSet s :=
by
convert (hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂)
simp [image_preimage_eq_range_inter, ← union_inter_distrib_right, univ_subset_iff.1 h]
