exists_seq_strictAnti_tendsto — Mathlib

English

Let f: β → α with dense range. For x < y, there exists u: ℕ → β such that f(u_n) ∈ Ioo x y for all n, and Tendsto (f ∘ u) to x.

Русский

При плотном образе существует такая последовательность.

LaTeX

$$$$\exists u: \mathbb{N} \to \beta,\; \text{StrictAnti}(u) \wedge (\forall n, f(u_n) \in Ioo(x,y)) \\wedge \operatorname{Tendsto}(f \circ u)\ atTop\ (\mathcal{N} x).$$$$

Lean4

theorem exists_seq_strictAnti_tendsto {β : Type*} [LinearOrder β] [DenselyOrdered α] [NoMaxOrder α]
    [FirstCountableTopology α] {f : β → α} (hf : DenseRange f) (hmono : Monotone f) (x : α) :
    ∃ u : ℕ → β, StrictAnti u ∧ (∀ n, f (u n) ∈ Ioi x) ∧ Tendsto (f ∘ u) atTop (𝓝 x) :=
  hf.exists_seq_strictMono_tendsto (α := αᵒᵈ) (β := βᵒᵈ) hmono.dual x

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