blimsup_false — Mathlib

English

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

Русский

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

LaTeX

$$$\\mathrm{blimsup}(u,f,\\lambda x.\\mathrm{False}) = \\bot$$$

Lean4

@[simp]
theorem blimsup_false {f : Filter β} {u : β → α} : (blimsup u f fun _ => False) = ⊥ := by simp [blimsup_eq]

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