sup_limsup — Mathlib

English

For a fixed a in α and NeBot filter f, a ⊔ limsup u f = limsup (a ⊔ u) f.

Русский

Для фиксированного a ∈ α и NeBot фильтра f выполняется a ⊔ limsup u f = limsup (a ⊔ u) f.

LaTeX

$$$\\operatorname{sup}(a, \\operatorname{limsup} u f) = \\operatorname{limsup}(a \\sqcup u) f$$$

Lean4

theorem sup_limsup [NeBot f] (a : α) : a ⊔ limsup u f = limsup (fun x => a ⊔ u x) f :=
  by
  simp only [limsup_eq_iInf_iSup, iSup_sup_eq, sup_iInf₂_eq]
  congr; ext s; congr; ext hs; congr
  exact (biSup_const (nonempty_of_mem hs)).symm

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