Commit 2021-11-11 09:29 d5964a9a

feat(measure_theory): int.floor etc are measurable (#10265)

API changes

algebra/order/archimedean

• rename rat.cast_floor to rat.floor_cast to reflect the order of operations;
• same for rat.cast_ceil and rat.cast_round;
• add rat.cast_fract.

algebra/order/floor

• add @[simp] to nat.floor_eq_zero;
• add nat.floor_eq_iff', nat.preimage_floor_zero, and nat.preimage_floor_of_ne_zero;
• add nat.ceil_eq_iff, nat.preimage_ceil_zero, and nat.preimage_ceil_of_ne_zero;
• add int.preimage_floor_singleton;
• add int.self_sub_floor, int.fract_int_add, int.preimage_fract, int.image_fract;
• add int.preimage_ceil_singleton.

measure_theory/function/floor

New file. Prove that the functions defined in algebra.order.floor are measurable.