tendsto_pi — Mathlib

English

Let f, m, l be as above. Then Tendsto m l (pi f) is equivalent to coordinatewise Tendsto: for every i, Tendsto (fun x => m x i) l (f i).

Русский

Пусть f, m, l заданы так же. Тогда Tendsto m l (pi f) эквивалентно поперечному пределу по координатам: для каждого i имеет место Tendsto (λ x. m x i) l (f i).

LaTeX

$$$\operatorname{Tendsto} m\ l\ (\pi f) \iff \forall i, \operatorname{Tendsto}(\lambda x. m\,x\,i)\ l\ (f_i).$$$

Lean4

theorem tendsto_pi {β : Type*} {m : β → ∀ i, α i} {l : Filter β} :
    Tendsto m l (pi f) ↔ ∀ i, Tendsto (fun x => m x i) l (f i) := by simp only [pi, tendsto_iInf, tendsto_comap_iff];
  rfl

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