tendsto_atBot_principal — Mathlib

English

For any set s, Tendsto f atBot (principal s) is equivalent to the existence of an N such that for all n ≤ N, f(n) ∈ s.

Русский

Для множества s, Tendsto f atBot (principal s) эквивалентно существованию N, такого что для всех n ≤ N, f(n) ∈ s.

LaTeX

$$$\text{Tendsto } f\ atBot (\mathcal{P} s) \leftrightarrow \exists N, \forall n \le N, f(n) \in s$$$

Lean4

theorem tendsto_atBot_principal {s : Set β} : Tendsto f atBot (𝓟 s) ↔ ∃ N, ∀ n ≤ N, f n ∈ s :=
  tendsto_atTop_principal (α := αᵒᵈ) (β := βᵒᵈ)

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