coprod_mono — Mathlib

English

If f1 ≤ f2 and g1 ≤ g2 as filters, then f1.coprod g1 ≤ f2.coprod g2.

Русский

Если f1 ≤ f2 и g1 ≤ g2 как фильтры, то f1.coprod g1 ≤ f2.coprod g2.

LaTeX

$$$ f_1 \le f_2 \quad\text{and}\quad g_1 \le g_2 \quad\Rightarrow\quad f_1 \coprod g_1 \le f_2 \coprod g_2 $$$

Lean4

@[mono]
theorem coprod_mono {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : f₁.coprod g₁ ≤ f₂.coprod g₂ :=
  sup_le_sup (comap_mono hf) (comap_mono hg)

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