Theorems · Theorem · real analysis

ENNReal.limsup_liminf_le_liminf_limsup

∀ {α : Type u_1} {β : Type u_2} [Countable β] {f : Filter α} [CountableInterFilter f] {g : Filter β}
  (u : α → β → ENNReal),
  Filter.limsup (fun a => Filter.liminf (fun b => u a b) g) f ≤
    Filter.liminf (fun b => Filter.limsup (fun a => u a b) f) g

Defined in

Mathlib.Order.Filter.ENNReal

Cited by

1 results in Mathlib

Foundations

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

Assumes

CountableCountableInterFilter