α : Type u_2
β : Type u_1
γ : Type ?u.176193
ι : Type ?u.176196
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : NeBot f
a : α
⊢ (a \ limsup u f)ᶜ = liminf (fun b => a \ u b) fᶜ
α : Type u_2
β : Type u_1
γ : Type ?u.176193
ι : Type ?u.176196
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : NeBot f
a : α
⊢ a \ limsup u f = liminf (fun b => a \ u b) f
rw [← compl_inj_iff]