congr — Mathlib

English

If s is BaireMeasurableSet and s and t are almost equal (mod residual), then t is BaireMeasurableSet.

Русский

Если множество s Баирово измеримо и s эквивалентно t по резидуальному эквиваленту (почти одинаковы в мерах), то t тоже Баирово измеримо.

LaTeX

$$$$ \mathrm{BaireMeasurableSet}(s) \rightarrow (s =\!\!\!\!_{\text{residual}} t) \rightarrow \mathrm{BaireMeasurableSet}(t). $$$$

Lean4

theorem congr (hs : BaireMeasurableSet s) (h : s =ᵇ t) : BaireMeasurableSet t :=
  EventuallyMeasurableSet.congr (α := α) hs h.symm

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