bliminf_eq_liminf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem bliminf_eq_liminf {f : Filter β} {u : β → α} {p : β → Prop} : bliminf u f p = liminf u (f ⊓ 𝓟 {x | p x}) :=
  blimsup_eq_limsup (α := αᵒᵈ)

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