congr — Mathlib

English

If f is EventuallyMeasurable and g equals f almost everywhere with respect to l, then g is EventuallyMeasurable.

Русский

Если fEventuallyMeasurable, и g эквивалентно f почти всюду по l, то g также EventuallyMeasurable.

LaTeX

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

Lean4

/-- A function which is `EventuallyEq` to some `EventuallyMeasurable` function
is `EventuallyMeasurable`. -/
theorem congr (hf : EventuallyMeasurable m l f) (hgf : g =ᶠ[l] f) : EventuallyMeasurable m l g := fun _ hs =>
  EventuallyMeasurableSet.congr (hf hs) (hgf.preimage _)

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