liminf_compl — Mathlib

English

In a complete Boolean algebra, the complement of a liminf equals the limsup of the complements.

Русский

В полном булеановом алгебре комплемент лиминфа равен лимсупу комплементов.

LaTeX

$$$(\\liminf u f)^c = \\limsup (\\\\circ c \\,\\circ u) f$$$

Lean4

theorem liminf_compl : (liminf u f)ᶜ = limsup (compl ∘ u) f := by
  simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]

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