bliminf_false — Mathlib

English

The bliminf of a function along a filter with the predicate constantly false is the top element: bliminf u f (λ x, False) = ⊤.

Русский

Блиминф функции вдоль фильтра с ложным условием равен верхнему элементу: bliminf u f (λ x, False) = ⊤.

LaTeX

$$$\\mathrm{bliminf}(u,f,\\lambda x.\\mathrm{False}) = \\top$$$

Lean4

@[simp]
theorem bliminf_false {f : Filter β} {u : β → α} : (bliminf u f fun _ => False) = ⊤ := by simp [bliminf_eq]

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