measurable_fract — Mathlib

English

If f is measurable, then the fract function applied to f is measurable (fract takes fractional part).

Русский

Если f измерима, то fract(f) измерима (дробная часть).

LaTeX

$$$$ \text{Measurable }( \operatorname{Int.fract} \circ f ). $$$$

Lean4

theorem measurable_fract [IsStrictOrderedRing R] [BorelSpace R] : Measurable (Int.fract : R → R) :=
  by
  intro s hs
  rw [Int.preimage_fract]
  exact MeasurableSet.iUnion fun z => measurable_id.sub_const _ (hs.inter measurableSet_Ico)

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