exists_seq_strictAnti_tendsto_of_lt

English

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

Русский

Если образ отображения густо в α, существует Such последовательность.

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_of_lt {β : Type*} [LinearOrder β] [DenselyOrdered α] [FirstCountableTopology α]
    {f : β → α} {x y : α} (hf : DenseRange f) (hmono : Monotone f) (hlt : x < y) :
    ∃ u : ℕ → β, StrictAnti u ∧ (∀ n, f (u n) ∈ Ioo x y) ∧ Tendsto (f ∘ u) atTop (𝓝 x) := by
  simpa using hf.exists_seq_strictMono_tendsto_of_lt (α := αᵒᵈ) (β := βᵒᵈ) hmono.dual (OrderDual.toDual_lt_toDual.2 hlt)

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