exists_seq_rat_strictMono_tendsto

English

There exists a strictly increasing sequence of rationals converging to x from below.

Русский

Существует строго возрастающая последовательность рациональных чисел, сходящаяся к x снизу.

LaTeX

$$$\exists u: \mathbb{N} \to \mathbb{Q},\; \text{StrictMono}(u) \land (\forall n, u(n) < x) \land \lim_{n\to\infty} u(n) = x$$$

Lean4

theorem exists_seq_rat_strictMono_tendsto (x : ℝ) :
    ∃ u : ℕ → ℚ, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto (u · : ℕ → ℝ) atTop (𝓝 x) :=
  Rat.denseRange_cast.exists_seq_strictMono_tendsto Rat.cast_strictMono.monotone x

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