liminf_set_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- In other words, `liminf cofinite s` is the set of elements lying outside the family `s`
finitely often. -/
theorem liminf_set_eq : liminf s cofinite = {x | {n | x ∉ s n}.Finite} := by
  simp only [← cofinite.bliminf_true s, cofinite.bliminf_set_eq, true_and]

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