prod_mono — Mathlib

English

The product operation is monotone in both arguments: if f1 ≤ f2 and g1 ≤ g2 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 \Rightarrow f_1 \times g_1 \le f_2 \times g_2.$$$$

Lean4

@[mono, gcongr]
theorem prod_mono {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂ :=
  inf_le_inf (comap_mono hf) (comap_mono hg)

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