sdiff_liminf — Mathlib

English

Same relation as above, stated for general u and f with complement in a Boolean algebra.

Русский

Та же связь, что и выше, для произвольной u и f в булевой алгебре.

LaTeX

$$$(\\limsup u f) \\setminus a = \\liminf (\\lambda b. u b \\setminus a) f$$$

Lean4

theorem sdiff_liminf (a : α) : a \ liminf u f = limsup (fun b => a \ u b) f :=
  by
  rw [← compl_inj_iff]
  simp only [sdiff_eq, limsup_compl, comp_def, compl_inf, compl_compl, sup_liminf]

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