tendsto_principal_Ici — Mathlib

English

If a is a minimal element with respect to f along a filter l, then f tends to the principal filter generated by the interval [f(a), ∞).

Русский

Если a является минимальным относительно f вдоль фильтра l, то f стремится к принципиальному фильтру, порождаемому интервалом [f(a), ∞).

LaTeX

$$$IsMinFilter\ f\ l\ a \to Tendsto\ f\ l\ (\mathcal{P}\ (Ici (f\ a)))$$$

Lean4

theorem tendsto_principal_Ici (h : IsMinFilter f l a) : Tendsto f l (𝓟 <| Ici (f a)) :=
  tendsto_principal.2 h

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