exists_seq_strictMono_tendsto_of_lt

English

Let s be a dense subset of α. For x > y, there exists a strictly increasing sequence u with all terms in Ioo(y, x) ∩ s, and u_n → x.

Русский

Плотное подмножество s в α: существует строго возрастающая последовательность внутри открытой окрестности слева от x, устремляющаяся к x.

LaTeX

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

Lean4

theorem exists_seq_strictMono_tendsto_of_lt [DenselyOrdered α] [FirstCountableTopology α] {s : Set α} (hs : Dense s)
    {x y : α} (hy : y < x) : ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ (Ioo y x ∩ s)) ∧ Tendsto u atTop (𝓝 x) :=
  by
  have hnonempty : (Ioo y x ∩ s).Nonempty :=
    by
    obtain ⟨z, hyz, hzx⟩ := hs.exists_between hy
    exact ⟨z, mem_inter hzx hyz⟩
  have hx : IsLUB (Ioo y x ∩ s) x := hs.isLUB_inter_iff isOpen_Ioo |>.mpr <| isLUB_Ioo hy
  apply hx.exists_seq_strictMono_tendsto_of_notMem (by simp) hnonempty |>.imp
  simp_all

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