English
Let s be a dense set in α. For x < y, there exists a strictly decreasing sequence u with all u_n ∈ Ioo y x ∩ s, converging to x from above.
Русский
Если s плотное в α, то для любых x < y существует строго убывающая последовательность внутри Ioo(y, x) ∩ s, сходящаяся к x сверху.
LaTeX
$$$$\exists u: \mathbb{N} \to \alpha,\; \text{StrictAnti}(u) \wedge (\forall n, u_n \in (Ioo(y, x) \cap s)) \\wedge \operatorname{Tendsto} u\ atTop\ (\mathcal{N} x).$$$$
Lean4
theorem exists_seq_strictAnti_tendsto' [DenselyOrdered α] [FirstCountableTopology α] {x y : α} (hy : x < y) :
∃ u : ℕ → α, StrictAnti u ∧ (∀ n, u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x) := by
simpa using exists_seq_strictMono_tendsto' (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)
