prod_mono_left — Mathlib

English

Let f1, f2 be filters on α and g be a filter on β. If f1 ≤ f2, then f1 × g ≤ f2 × g.

Русский

Пусть f1, f2 — фильтры на α и g — фильтр на β. Если f1 ≤ f2, то f1 × g ≤ f2 × g.

LaTeX

$$$\forall \alpha \beta\, (f_1,f_2 : \mathrm{Filter}(\alpha))\, (g : \mathrm{Filter}(\beta))\; (f_1 \le f_2) \Rightarrow f_1 \times g \le f_2 \times g$$$

Lean4

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

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