fract — Mathlib

English

There is a measurable floor map from ℝ to ℕ, i.e., Nat.floor is measurable.

Русский

Существует измеримая функция floor из ℝ в ℕ: Nat.floor измерима.

LaTeX

$$$$ \operatorname{Measurable} (\operatorname{Nat.floor} : \mathbb{R} \to \mathbb{N}). $$$$

Lean4

@[measurability, fun_prop]
theorem fract [IsStrictOrderedRing R] [BorelSpace R] {f : α → R} (hf : Measurable f) :
    Measurable fun x => Int.fract (f x) :=
  measurable_fract.comp hf

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