image_fract — Mathlib

English

If s is a measurable subset of R, then the image of s under fract is a measurable set.

Русский

Если s измеримо в R, то образ s под fract измерим.

LaTeX

$$$$ \operatorname{MeasurableSet}(s) \Rightarrow \operatorname{MeasurableSet}(\operatorname{Int.fract}'' s). $$$$

Lean4

theorem image_fract [IsStrictOrderedRing R] [BorelSpace R] {s : Set R} (hs : MeasurableSet s) :
    MeasurableSet (Int.fract '' s) :=
  by
  simp only [Int.image_fract, sub_eq_add_neg, image_add_right']
  exact MeasurableSet.iUnion fun m => (measurable_add_const _ hs).inter measurableSet_Ico

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