eventually_ne — Mathlib

English

If l is an exponential comparison filter, then almost all points w in l satisfy w ≠ 0.

Русский

Если фильтр l является экспоненциальным сравнительным, то почти все точки w из l не равны нулю.

LaTeX

$$$\\forall l:\\,\\mathsf{IsExpCmpFilter}\\ l\\ \\to\\; \\forall^{\\infty} w:\\; w \\neq 0\\text{ in } l$$$

Lean4

theorem eventually_ne (hl : IsExpCmpFilter l) : ∀ᶠ w : ℂ in l, w ≠ 0 :=
  hl.tendsto_re.eventually_ne_atTop' _

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