comp_eventuallyMeasurable — Mathlib

English

If h is measurable and f is EventuallyMeasurable, then h ∘ f is EventuallyMeasurable.

Русский

Если h измерима, а f является EventuallyMeasurable, то композиция h ∘ f тоже EventuallyMeasurable.

LaTeX

$$$\text{Measurable}(h) \Rightarrow (\text{EventuallyMeasurable}(m,l,f) \Rightarrow \text{EventuallyMeasurable}(m,l,h\circ f)).$$$

Lean4

theorem comp_eventuallyMeasurable (hh : Measurable h) (hf : EventuallyMeasurable m l f) :
    EventuallyMeasurable m l (h ∘ f) :=
  hh.comp hf

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