Theorems · Theorem · order theory

Filter.sdiff_limsup

∀ {α : Type u_1} {β : Type u_2} [inst : CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) [f.NeBot] (a : α),
  a \ Filter.limsup u f = Filter.liminf (fun b => a \ u b) f

Defined in

Mathlib.Order.LiminfLimsup

Cited by

0 results in Mathlib

Foundations

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

Assumes

CompleteBooleanAlgebraFilter.NeBot