exists_seq_strictAnti_tendsto_of_lt

English

Let s be dense in α. For x < y, there exists a strictly anti-monotone sequence u with u_n ∈ Ioo x y ∩ s and Tendsto u to 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_of_lt [DenselyOrdered α] [FirstCountableTopology α] {s : Set α} (hs : Dense s)
    {x y : α} (hy : x < y) : ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, u n ∈ (Ioo x y ∩ s)) ∧ Tendsto u atTop (𝓝 x) := by
  simpa using hs.exists_seq_strictMono_tendsto_of_lt (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)

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