Theorems · Theorem · order theory

Filter.liminf_sdiff

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

Defined in

Mathlib.Order.LiminfLimsup

Cited by

0 results in Mathlib

Foundations

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

Assumes

CompleteBooleanAlgebraFilter.NeBot