exists_seq_strictAnti_tendsto — Mathlib

English

Let x be in α. There exists a strictly anti-monotone sequence u with u_n ∈ Ioi x ∩ s and Tendsto (f ∘ u) to x within nhdsWithin x (Ioi x).

Русский

Существует последовательность в плотном подмножество, убывающая к x сверху в локальном смысле.

LaTeX

$$$$\exists u: \mathbb{N} \to \alpha,\; \text{StrictAnti}(u) \wedge (\forall n, u_n \in Ioi x \cap s) \\wedge \operatorname{Tendsto} (f \circ u)\ atTop\ (\mathcal{nhdsWithin} x (Ioi x)).$$$$

Lean4

theorem exists_seq_strictAnti_tendsto [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α] {s : Set α}
    (hs : Dense s) (x : α) : ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, u n ∈ (Ioi x ∩ s)) ∧ Tendsto u atTop (𝓝 x) :=
  hs.exists_seq_strictMono_tendsto (α := αᵒᵈ) x

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