inf_limsup — Mathlib

English

Let α be a complete distributive lattice. For any a ∈ α, any function u : β → α, and any filter f on β, the infimum of a with the limsup of u equals the limsup of the infimum with a: a ∧ limsup u f = limsup (λ x, a ∧ u x) f.

Русский

Пусть α — полная распределимая решётка. Для любого a ∈ α, функции u : β → α и фильтра f на β выполняется: a ∧ limsup u f = limsup (λ x, a ∧ u x) f.

LaTeX

$$$a \\wedge \\limsup u f = \\limsup (\\lambda x. a \\wedge u x) f$$$

Lean4

theorem inf_limsup (a : α) : a ⊓ limsup u f = limsup (fun x => a ⊓ u x) f :=
  sup_liminf (α := αᵒᵈ) a

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