tendsto_ceil_right_pure_floor_add_one

English

As x approaches from the right, ceil x tends to ⌊x⌋ + 1.

Русский

При подходе справа ceil x стремится к ⌊x⌋ + 1.

LaTeX

$$$$\lim_{y \to x^+} \lceil y \rceil = \lfloor x \rfloor + 1.$$$$

Lean4

theorem tendsto_ceil_right_pure_floor_add_one (x : α) : Tendsto (ceil : α → ℤ) (𝓝[>] x) (pure (⌊x⌋ + 1)) :=
  have : ↑(⌊x⌋ + 1) - 1 ≤ x := by rw [cast_add, cast_one, add_sub_cancel_right]; exact floor_le _
  tendsto_pure.2 <|
    mem_of_superset (Ioc_mem_nhdsGT <| lt_succ_floor _) fun _y hy => ceil_eq_on_Ioc _ _ ⟨this.trans_lt hy.1, hy.2⟩

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