bliminf_true — Mathlib

English

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

Русский

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

LaTeX

$$$ \\operatorname{bliminf}(u,f,\\mathbf{1}) = \\operatorname{liminf}(u,f) $$$

Lean4

@[simp]
theorem bliminf_true (f : Filter β) (u : β → α) : (bliminf u f fun _ => True) = liminf u f := by
  simp [bliminf_eq, liminf_eq]

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