exists_seq_antitone_tendsto_atTop_atBot

English

There exists a sequence xs: ℕ → α which is Antitone and tends to atBot along the natural-number index, under suitable directedness and countable generation conditions of atBot.

Русский

Существуют последовательность xs: ℕ → α,Antitone, такая что xs сходится к atBot вдоль atTop, при заданных условиях направленности и счетной генерации atBot.

LaTeX

$$$\\exists xs:\\mathbb{N} \\to \\alpha,\\; \\text{Antitone}\\ xs \\land \\operatorname{Tendsto}\\ xs\\ \\operatorname{atTop}\\ \\operatorname{atBot}$$$

Lean4

theorem exists_seq_antitone_tendsto_atTop_atBot (α : Type*) [Preorder α] [Nonempty α] [IsDirected α (· ≥ ·)]
    [(atBot : Filter α).IsCountablyGenerated] : ∃ xs : ℕ → α, Antitone xs ∧ Tendsto xs atTop atBot :=
  exists_seq_monotone_tendsto_atTop_atTop αᵒᵈ

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