tendsto_atTop_principal — Mathlib

English

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

Русский

Для любого множества s, сходиться функция f к главной фильтру на s эквивалентно существованию N такого, что для всех n ≥ N, f(n) ∈ s.

LaTeX

$$$(f : \alpha \to \beta)\ Tendsto f atTop (\mathcal{P} s) \leftrightarrow \exists N, \forall n \ge N, f(n) \in s$$$

Lean4

theorem tendsto_atTop_principal {s : Set β} : Tendsto f atTop (𝓟 s) ↔ ∃ N, ∀ n ≥ N, f n ∈ s := by
  simp_rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_atTop_sets, mem_preimage]

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