exists_seq_strictAnti_tendsto_nhdsWithin

English

Let s be a dense subset of α. For x < y with is bounded between, there exists a strictly antitone sequence u with u_n ∈ Ioo x y ∩ s and u_n → x.

Русский

Плотное множество: существует строго антимонотонная последовательность внутри интервала Ioo(x, y), сходящаяся к x.

LaTeX

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

Lean4

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

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