measurable_floor — Mathlib

English

Another version: Nat.floor is measurable for IsStrictOrderedRing contexts.

Русский

Альтернативно: Nat.floor измерима в контекстах IsStrictOrderedRing.

LaTeX

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

Lean4

theorem measurable_floor [IsStrictOrderedRing R] : Measurable (Nat.floor : R → ℕ) :=
  measurable_to_countable fun n => by
    rcases eq_or_ne ⌊n⌋₊ 0 with h | h <;> simp [h, Nat.preimage_floor_of_ne_zero, -floor_eq_zero]

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