blimsup_true — Mathlib

English

Let α be a ConditionallyCompleteLattice, f a filter on β, and u: β → α. Then the blimsup of u with respect to f along the constantly true predicate equals the limsup of u with respect to f.

Русский

Пусть α — условно завершаемая решетка, f — фильтр на β, и u: β → α. Тогда blimsup(u, f, True) равен limsup(u, f).

LaTeX

$$$ \\operatorname{blimsup}(u,f,\\mathbf{1}) = \\operatorname{limsup}(u,f) $$$

Lean4

@[simp]
theorem blimsup_true (f : Filter β) (u : β → α) : (blimsup u f fun _ => True) = limsup u f := by
  simp [blimsup_eq, limsup_eq]

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