limsup_set_eq — Mathlib

English

For the cofinite filter, limsup s cofinite equals the set of x such that {n | x ∈ s n} is Infinite.

Русский

Для cofinite limsup s cofinite — множество x, таких что {n | x ∈ s_n} бесконечно.

LaTeX

$$limsup s cofinite = {x | {n | x ∈ s n}.Infinite}$$

Lean4

/-- In other words, `limsup cofinite s` is the set of elements lying inside the family `s`
infinitely often. -/
theorem limsup_set_eq : limsup s cofinite = {x | {n | x ∈ s n}.Infinite} := by
  simp only [← cofinite.blimsup_true s, cofinite.blimsup_set_eq, true_and]

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