English
If u is frequently nonnegative and both u and v are f-bounded under ≤ with nonnegativity and monotonicity conditions for multiplication, then u·v is f-bounded under ≤.
Русский
Если u часто неотрицательно и оба u, v ограничены снизу по ≤, а умножение удовлетворяет монотонности, то u·v ограничено снизу по ≤ вдоль фильтра.
LaTeX
$$$\exists ⟨U, hU⟩, \exists ⟨V, hV⟩, f.IsBoundedUnder(≤)\ u, f.IsBoundedUnder(≤)\ v \Rightarrow f.IsBoundedUnder(≤)\ (u\cdot v)$$$
Lean4
theorem isBoundedUnder_le_mul_of_nonneg [Preorder α] [Mul α] [Zero α] [PosMulMono α] [MulPosMono α] {f : Filter ι}
{u v : ι → α} (h₁ : ∃ᶠ x in f, 0 ≤ u x) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v)
(h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v) : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v) :=
by
obtain ⟨U, hU⟩ := h₂.eventually_le
obtain ⟨V, hV⟩ := h₄.eventually_le
refine isBoundedUnder_of_eventually_le (a := U * V) ?_
filter_upwards [hU, hV, h₃] with x x_U x_V v_0
have U_0 : 0 ≤ U := by
obtain ⟨y, y_0, y_U⟩ := (h₁.and_eventually hU).exists
exact y_0.trans y_U
exact (mul_le_mul_of_nonneg_right x_U v_0).trans (mul_le_mul_of_nonneg_left x_V U_0)
