Theorems · Theorem · general topology

le_limsup_mul

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

Defined in

Mathlib.Topology.Algebra.Order.LiminfLimsup

Cited by

0 results in Mathlib

Foundations

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