English
In a Boolean algebra, the sdiff with limsup equals the liminf of sdiffs with the arguments: a \\ limsup u f = liminf (λ b. a \\ u b) f.
Русский
В булевой алгебре разность по отношению к лимсупу равна лимину от разностей: a \\ limsup u f = liminf (λ b. a \\ u b) f.
LaTeX
$$$a \\setminus (\\limsup u f) = \\liminf (\\lambda b. a \\setminus u b) f$$$
Lean4
theorem sdiff_limsup [NeBot f] (a : α) : a \ limsup u f = liminf (fun b => a \ u b) f :=
by
rw [← compl_inj_iff]
simp only [sdiff_eq, liminf_compl, comp_def, compl_inf, compl_compl, sup_limsup]