exists_seq_strictAnti_tendsto — Mathlib

English

For densely ordered α with no maximum and first-countable topology, there exists a strictly anti-monotone sequence u with x < u_n for all n and u_n → x.

Русский

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

LaTeX

$$$$\exists u: \mathbb{N} \to \alpha,\; \text{StrictAnti}(u) \wedge (\forall n, x < u_n) \wedge \operatorname{Tendsto} u\ atTop\ (\mathcal{N} x).$$$$

Lean4

theorem exists_seq_strictAnti_tendsto [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α] (x : α) :
    ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, x < u n) ∧ Tendsto u atTop (𝓝 x) :=
  exists_seq_strictMono_tendsto (α := αᵒᵈ) x

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