measurable_of_measurable_on_compl_finite

English

If s is finite and (sᶜ.restrict f) is measurable, then f is measurable.

Русский

Если s конечное и (sᶜ.ограничение f) измеримо, то f измеримо.

LaTeX

$$$\\\\operatorname{Measurable}(s^c\\\\\\\\text{restrict } f) \\\\Rightarrow \\\\operatorname{Measurable} f$$$

Lean4

theorem measurable_of_measurable_on_compl_finite [MeasurableSingletonClass α] {f : α → β} (s : Set α) (hs : s.Finite)
    (hf : Measurable (sᶜ.restrict f)) : Measurable f :=
  have := hs.to_subtype
  measurable_of_restrict_of_restrict_compl hs.measurableSet (measurable_of_finite _) hf

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