mul_le_mul' — Mathlib

English

If f1 ≤ᶠ[l] f2 and g1 ≤ᶠ[l] g2 with g1 ≥ 0 and f2 ≥ 0 eventually, then f1*g1 ≤ᶠ[l] f2*g2.

Русский

Если f1 ≤ᶠ[l] f2 и g1 ≤ᶠ[l] g2 при условии g1 ≥ 0 и f2 ≥ 0, то f1*g1 ≤ᶠ[l] f2*g2.

LaTeX

$$$ f_1 \le^\!{l} f_2 \quad \land \quad g_1 \le^\!{l} g_2 \quad \land \ 0 \le^\!{l} g_1 \quad \land \ 0 \le^\!{l} f_2 \Rightarrow f_1 * g_1 \le^\!{l} f_2 * g_2 $$$

Lean4

@[to_additive EventuallyLE.add_le_add]
theorem mul_le_mul' [Mul β] [Preorder β] [MulLeftMono β] [MulRightMono β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β}
    (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂ := by
  filter_upwards [hf, hg] with x hfx hgx using _root_.mul_le_mul' hfx hgx

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