blimsup_eq_limsup — Mathlib

English

Let α be a ConditionallyCompleteLattice, f: Filter β, u: β → α, and p: β → Prop. Then blimsup u f p equals limsup u (f ⊓ 𝓟{ x | p x }).

Русский

Пусть α — условно завершенная решетка, f: фильтр β, u: β → α, p: β → Prop. Тогда blimsup u f p равен limsup u (f ⊓ 𝓟{ x | p x }).

LaTeX

$$$ \\operatorname{blimsup} u f p = \\operatorname{limsup} u (f \\inf \\mathcal{P}\\{ x \\mid p(x) \\}) $$$

Lean4

theorem blimsup_eq_limsup {f : Filter β} {u : β → α} {p : β → Prop} : blimsup u f p = limsup u (f ⊓ 𝓟 {x | p x}) := by
  simp only [blimsup_eq, limsup_eq, eventually_inf_principal, mem_setOf_eq]

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