prodMap — Mathlib

English

If f1 ≤ f2 and g1 ≤ g2 for filters, then f1 × g1 ≤ f2 × g2.

Русский

Если f1 ≤ f2 и g1 ≤ g2 для фильтров, то f1 × g1 ≤ f2 × g2.

LaTeX

$$$$f_1 \le f_2 \quad\text{и}\quad g_1 \le g_2 \quad\Rightarrow\quad f_1 \times g_1 \le f_2 \times g_2.$$$$

Lean4

theorem prodMap {δ} [LE γ] [LE δ] {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

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