prodMap — Mathlib

English

If fa ≈ ga eventually on la and fb ≈ gb eventually on lb, then Prod.map fa fb ≈ Prod.map ga gb eventually on la ×ˢ lb.

Русский

Если fa эквивалентно ga в пределе ла и fb эквивалентно gb в lb, то Prod.map fa fb эквивалентно Prod.map ga gb на ла × lb.

LaTeX

$$$$\text{la.EventuallyEq fa ga} \rightarrow (\text{lb.EventuallyEq fb gb} \rightarrow (\text{Prod.map fa fb} =_{{la \times lb}} \text{Prod.map ga gb})).$$$$

Lean4

theorem prodMap {δ} {la : Filter α} {fa ga : α → γ} (ha : fa =ᶠ[la] ga) {lb : Filter β} {fb gb : β → δ}
    (hb : fb =ᶠ[lb] gb) : Prod.map fa fb =ᶠ[la ×ˢ lb] Prod.map ga gb :=
  (Eventually.prod_mk ha hb).mono fun _ h => Prod.ext h.1 h.2

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