Theorems · Theorem · order theory

Filter.sup_limsup

∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {u : β → α} [f.NeBot] (a : α),
  a ⊔ Filter.limsup u f = Filter.limsup (fun x => a ⊔ u x) f

Defined in

Mathlib.Order.LiminfLimsup

Cited by

2 results in Mathlib

Foundations

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

Assumes

CompleteDistribLatticeFilter.NeBot