tendsto_principal_Iic — Mathlib

English

If a is a maximal 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

$$$IsMaxFilter\ f\ l\ a \to Tendsto\ f\ l\ (\mathcal{P}\ (Iic (f\ a)))$$$

Lean4

theorem tendsto_principal_Iic (h : IsMaxFilter f l a) : Tendsto f l (𝓟 <| Iic (f a)) :=
  tendsto_principal.2 h

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