le_pi — Mathlib

English

For any g : Filter (∀ i, α_i), g ≤ pi f if and only if for all i, Tendsto eval i from g to f i.

Русский

Для любого g: фильтр на продукт ∀ i, α_i имеет место g ≤ π f тогда и только тогда, когда для каждого i выполнено Tendsto eval_i: g → f_i.

LaTeX

$$$g \le \pi f \iff \forall i, \operatorname{Tendsto}(\mathrm{eval}_i)\ g\ (f_i).$$$

Lean4

theorem le_pi {g : Filter (∀ i, α i)} : g ≤ pi f ↔ ∀ i, Tendsto (eval i) g (f i) :=
  tendsto_pi

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