English
There exist two sequences u and v in α: u is strictly anti-monotone tending to x, v is strictly monotone tending to y, with all u_n, v_n lying in Ioo x y, and each u_k < v_l, together with Tendsto conditions.
Русский
Существуют две последовательности, одна из которых строгоAnti стремится к x снизу, другая строгоMono стремится к y сверху, и все элементы лежат внутри открытого отрезка (x,y).
LaTeX
$$$$\exists u, v:\mathbb{N}\to \alpha,\; \text{StrictAnti}(u) \wedge \text{StrictMono}(v) \wedge (\forall k\, u_k \in Ioo(x,y)) \wedge (\forall l\, v_l \in Ioo(x,y)) \\wedge (\forall k,l,\, u_k < v_l) \wedge \operatorname{Tendsto} u\ atTop\ (\mathcal{N} x) \wedge \operatorname{Tendsto} v\ atTop\ (\mathcal{N} y).$$$$
Lean4
theorem exists_seq_strictAnti_strictMono_tendsto [DenselyOrdered α] [FirstCountableTopology α] {x y : α} (h : x < y) :
∃ u v : ℕ → α,
StrictAnti u ∧
StrictMono v ∧
(∀ k, u k ∈ Ioo x y) ∧
(∀ l, v l ∈ Ioo x y) ∧ (∀ k l, u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y) :=
by
rcases exists_seq_strictAnti_tendsto' h with ⟨u, hu_anti, hu_mem, hux⟩
rcases exists_seq_strictMono_tendsto' (hu_mem 0).2 with ⟨v, hv_mono, hv_mem, hvy⟩
exact
⟨u, v, hu_anti, hv_mono, hu_mem, fun l => ⟨(hu_mem 0).1.trans (hv_mem l).1, (hv_mem l).2⟩, fun k l =>
(hu_anti.antitone (zero_le k)).trans_lt (hv_mem l).1, hux, hvy⟩
