limsup_const_bot — Mathlib

English

The limsup of a constant bottom function is bottom: limsup (λ x, ⊥) f = ⊥ for any filter f.

Русский

Лимсуп константы ⊥ равен ⊥: limsup (λ x, ⊥) f = ⊥ для любого фильтра f.

LaTeX

$$$\\limsup (\\lambda x. \\bot) f = \\bot$$$

Lean4

/-- Same as limsup_const applied to `⊥` but without the `NeBot f` assumption -/
@[simp]
theorem limsup_const_bot {f : Filter β} : limsup (fun _ : β => (⊥ : α)) f = (⊥ : α) :=
  by
  rw [limsup_eq, eq_bot_iff]
  exact sInf_le (Eventually.of_forall fun _ => le_rfl)

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