exists_seq_rat_strictAnti_tendsto

English

There exists a strictly decreasing sequence of rationals converging to x from above.

Русский

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

LaTeX

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

Lean4

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

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