prodMk — Mathlib

English

If m1 tends to g and m2 tends to h along f, then the map x ↦ (m1 x, m2 x) tends to g × h along f.

Русский

Если m1 сходится к g и m2 сходится к h по f, то отображение x ↦ (m1 x, m2 x) сходится к g × h по f.

LaTeX

$$$$\operatorname{Tendsto}\, (\lambda x. (m_1 x, m_2 x))\ f\ (g \times g).$$$$

Lean4

theorem prodMk {h : Filter γ} {m₁ : α → β} {m₂ : α → γ} (h₁ : Tendsto m₁ f g) (h₂ : Tendsto m₂ f h) :
    Tendsto (fun x => (m₁ x, m₂ x)) f (g ×ˢ h) :=
  tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩

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