prod_mono_right — Mathlib

English

Let f be a filter on α and g1, g2 be filters on β. If g1 ≤ g2, then f × g1 ≤ f × g2.

Русский

Пусть f — фильтр на α и g1, g2 — фильтры на β. Если g1 ≤ g2, то f × g1 ≤ f × g2.

LaTeX

$$$\forall \alpha \beta\, (f : \mathrm{Filter}(\alpha))\, (g_1,g_2 : \mathrm{Filter}(\beta))\; (g_1 \le g_2) \Rightarrow f \times g_1 \le f \times g_2$$$

Lean4

theorem prod_mono_right (f : Filter α) {g₁ g₂ : Filter β} (hf : g₁ ≤ g₂) : f ×ˢ g₁ ≤ f ×ˢ g₂ :=
  Filter.prod_mono rfl.le hf

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