of_union_cover — Mathlib

English

If s and t are measurable and univ is covered by s ∪ t, and certain preimages are measurable, then u is measurable.

Русский

Если s и t измеримы и множество единица покрыто s ∪ t, а некоторые предобразные множества измеримы, то u измеримо.

LaTeX

$$$\\\\operatorname{MeasurableSet}(u)$, given hs, ht, h, hsu, htu$$

Lean4

theorem of_union_cover {s t u : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (h : univ ⊆ s ∪ t)
    (hsu : MeasurableSet (((↑) : s → α) ⁻¹' u)) (htu : MeasurableSet (((↑) : t → α) ⁻¹' u)) : MeasurableSet u :=
  by
  convert (hs.subtype_image hsu).union (ht.subtype_image htu)
  simp [image_preimage_eq_inter_range, ← inter_union_distrib_left, univ_subset_iff.1 h]

Похожие утверждения