prodMk — Mathlib

English

If HasProd f a and HasProd g b hold, then the product map x ↦ (f x, g x) has product (a, b).

Русский

Если HasProd f a и HasProd g b, то функция x ↦ (f x, g x) имеет произведение (a, b).

LaTeX

$$$\\forall f:\\beta\\to\\alpha\\,\\forall g:\\beta\\to\\gamma\\,\\forall a\\,\\forall b,\\ HasProd f a L \\land HasProd g b L \\Rightarrow HasProd (\\lambda x, (f x, g x)) (a, b) L$$$

Lean4

@[to_additive HasSum.prodMk]
theorem prodMk {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : HasProd f a L) (hg : HasProd g b L) :
    HasProd (fun x ↦ (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩ L := by
  simp [HasProd, ← prod_mk_prod, Filter.Tendsto.prodMk_nhds hf hg]

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