English
If 0 ≤ᶠ u and 0 ≤ᶠ v and u is f-bounded below while v is f-cobounded below, then u·v is f-cobounded below.
Русский
Если по фильтру f почти везде u и v неотрицательны, и u ограничен снизу, а v кобондированно ограничен снизу, то произведение u·v ограничено снизу.
LaTeX
$$$0 ≤ᶠ[f] u \land f.IsBoundedUnder(≤)\ u \land 0 ≤ᶠ[f] v \land f.IsCoboundedUnder(≤)\ v \Rightarrow f.IsCoboundedUnder(≤)\ (u\cdot v)$$$
Lean4
theorem isCoboundedUnder_ge_mul_of_nonneg [LinearOrder α] [Mul α] [Zero α] [PosMulMono α] [MulPosMono α] {f : Filter ι}
[f.NeBot] {u v : ι → α} (h₁ : 0 ≤ᶠ[f] u) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v)
(h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f (u * v) :=
by
obtain ⟨U, hU⟩ := h₂.eventually_le
obtain ⟨V, hV⟩ := h₄.frequently_le
refine IsCoboundedUnder.of_frequently_le (a := U * V) ?_
apply (hV.and_eventually (hU.and (h₁.and h₃))).mono
intro x ⟨x_V, x_U, u_0, v_0⟩
exact (mul_le_mul_of_nonneg_right x_U v_0).trans (mul_le_mul_of_nonneg_left x_V (u_0.trans x_U))
