measurable_of_measurable_union_cover

English

If s and t are measurable and univ ⊆ s ∪ t, then a certain u is measurable via subtypes.

Русский

Если s и t измеримы и univ ⊆ s ∪ t, то множество u измеримо.

LaTeX

$$$\\\\operatorname{MeasurableSet}(u)$$$

Lean4

theorem measurable_of_measurable_union_cover {f : α → β} (s t : Set α) (hs : MeasurableSet s) (ht : MeasurableSet t)
    (h : univ ⊆ s ∪ t) (hc : Measurable fun a : s => f a) (hd : Measurable fun a : t => f a) : Measurable f :=
  fun _u hu => .of_union_cover hs ht h (hc hu) (hd hu)

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