# Measurability of ⌊x⌋ etc #

In this file we prove that Int.floor, Int.ceil, Int.fract, Nat.floor, and Nat.ceil are measurable under some assumptions on the (semi)ring.

theorem Int.measurable_floor {R : Type u_2} [] [] [] [] :
Measurable Int.floor
theorem Measurable.floor {α : Type u_1} {R : Type u_2} [] [] [] [] [] {f : αR} (hf : ) :
Measurable fun (x : α) => f x
theorem Int.measurable_ceil {R : Type u_2} [] [] [] [] :
Measurable Int.ceil
theorem Measurable.ceil {α : Type u_1} {R : Type u_2} [] [] [] [] [] {f : αR} (hf : ) :
Measurable fun (x : α) => f x
theorem measurable_fract {R : Type u_2} [] [] [] [] [] :
Measurable Int.fract
theorem Measurable.fract {α : Type u_1} {R : Type u_2} [] [] [] [] [] [] {f : αR} (hf : ) :
Measurable fun (x : α) => Int.fract (f x)
theorem MeasurableSet.image_fract {R : Type u_2} [] [] [] [] [] {s : Set R} (hs : ) :
MeasurableSet (Int.fract '' s)
theorem Nat.measurable_floor {R : Type u_2} [] [] [] [] :
Measurable Nat.floor
theorem Measurable.nat_floor {α : Type u_1} {R : Type u_2} [] [] [] [] [] {f : αR} (hf : ) :
Measurable fun (x : α) => f x⌋₊
theorem Nat.measurable_ceil {R : Type u_2} [] [] [] [] :
Measurable Nat.ceil
theorem Measurable.nat_ceil {α : Type u_1} {R : Type u_2} [] [] [] [] [] {f : αR} (hf : ) :
Measurable fun (x : α) => f x⌉₊