congr — Mathlib

English

If s is μ-null measurable and s and t are μ-almost everywhere equal, then t is μ-null measurable.

Русский

Если s μ-нулеизмеримо и s равно t μ-почти всюду, то и t μ-нулеизмеримо.

LaTeX

$$NullMeasurableSet(s,\mu) \land s =^\mu t \Rightarrow NullMeasurableSet(t,\mu)$$

Lean4

protected theorem congr (hs : NullMeasurableSet s μ) (h : s =ᵐ[μ] t) : NullMeasurableSet t μ :=
  EventuallyMeasurableSet.congr hs h.symm

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