sdiff_limsup — Mathlib

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]

Похожие утверждения