eventuallyMeasurable_of_eventuallyEq

English

If f is measurable and g is eventually equal to f, then g is EventuallyMeasurable.

Русский

Если f измерима, а g совпадает с f в пределе (по l), то g является EventuallyMeasurable.

LaTeX

$$$\text{Measurable}(f) \land g =^l f \Rightarrow \text{EventuallyMeasurable}(m,l,g).$$$

Lean4

/-- A function which is `EventuallyEq` to some `Measurable` function is `EventuallyMeasurable`. -/
theorem eventuallyMeasurable_of_eventuallyEq (hf : Measurable f) (hgf : g =ᶠ[l] f) : EventuallyMeasurable m l g :=
  hf.eventuallyMeasurable.congr hgf

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