English
Let s be dense in α. For x < y there exists u: ℕ→α with u_n ∈ Ioo x y and Tendsto u to x from above, with u strictly anti-monotone.
Русский
Для плотного подмножеств найдётся strictlyAnti последовательность внутри промежутка (x,y), сходящаяся к x.
LaTeX
$$$$\exists u: \mathbb{N} \to \alpha,\; \text{StrictAnti}(u) \wedge (\forall n, u_n \in Ioo(x,y)) \\wedge \operatorname{Tendsto} u\ atTop (\mathcal{N} x).$$$$
Lean4
theorem exists_seq_tendsto_sInf {α : Type*} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α]
[FirstCountableTopology α] {S : Set α} (hS : S.Nonempty) (hS' : BddBelow S) :
∃ u : ℕ → α, Antitone u ∧ Tendsto u atTop (𝓝 (sInf S)) ∧ ∀ n, u n ∈ S :=
exists_seq_tendsto_sSup (α := αᵒᵈ) hS hS'
