seq_mono — Mathlib

English

If f1 ≤ f2 and g1 ≤ g2 then f1.seq g1 ≤ f2.seq g2.

Русский

Если f1 ≤ f2 и g1 ≤ g2, тогда f1.seq g1 ≤ f2.seq g2.

LaTeX

$$$ \text{if } f_1 \le f_2 \text{ and } g_1 \le g_2, \; f_1 \text{.seq } g_1 \le f_2 \text{.seq } g_2$$$

Lean4

@[mono]
theorem seq_mono {f₁ f₂ : Filter (α → β)} {g₁ g₂ : Filter α} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : f₁.seq g₁ ≤ f₂.seq g₂ :=
  le_seq fun _ hs _ ht => seq_mem_seq (hf hs) (hg ht)

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