tendsto_floor_left_pure_ceil_sub_one

English

As x approaches from the left of n, floor x approaches ⌈x⌉ − 1 from above with the same left neighborhood considerations.

Русский

При подходе слева к n, floor x приближается к ⌈x⌉ − 1 сверху в аналогичных левых окрестностях.

LaTeX

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

Lean4

theorem tendsto_floor_left_pure_ceil_sub_one (x : α) : Tendsto (floor : α → ℤ) (𝓝[<] x) (pure (⌈x⌉ - 1)) :=
  have h₁ : ↑(⌈x⌉ - 1) < x := by rw [cast_sub, cast_one, sub_lt_iff_lt_add]; exact ceil_lt_add_one _
  have h₂ : x ≤ ↑(⌈x⌉ - 1) + 1 := by rw [cast_sub, cast_one, sub_add_cancel]; exact le_ceil _
  tendsto_pure.2 <| mem_of_superset (Ico_mem_nhdsLT h₁) fun _y hy => floor_eq_on_Ico _ _ ⟨hy.1, hy.2.trans_le h₂⟩

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