Theorems · Theorem · general topology

Filter.isBoundedUnder_le_mul_of_nonneg

∀ {α : Type u_1} {ι : Type u_4} [inst : Preorder α] [inst_1 : Mul α] [inst_2 : Zero α] [PosMulMono α] [MulPosMono α]
  {f : Filter ι} {u v : ι → α},
  (∃ᶠ (x : ι) in f, 0 ≤ u x) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u →
      0 ≤ᶠ[f] v →
        Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)

Defined in

Mathlib.Order.Filter.IsBounded

Cited by

2 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderMulZeroPosMulMonoMulPosMono