isEquivalent_nat_ceil — Mathlib

English

The ceiling map is asymptotically equivalent to the identity on atTop.

Русский

Округление вверх по асимптотике эквивалентно тождественному отображению на бесконечности.

LaTeX

$$$\mathrm{isEquivalent}(\, x \mapsto \lceil x \rceil) \sim (\, x \mapsto x\,)$$$

Lean4

theorem isEquivalent_nat_ceil : (fun (x : R) ↦ ↑⌈x⌉₊) ~[atTop] (fun x ↦ x) :=
  by
  refine isEquivalent_of_tendsto_one ?_ tendsto_nat_ceil_div_atTop
  filter_upwards with x hx using by rw [hx, Nat.ceil_zero, Nat.cast_eq_zero]

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