Theorems · Theorem · general topology

limsup_mul_le

∀ {ι : Type u_1} {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.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f

Defined in

Mathlib.Topology.Algebra.Order.LiminfLimsup

Cited by

1 results in Mathlib

Foundations

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