English
For any filter f on β and p, the limsup of f ⊔ g equals the join of the limsups: limsup u (f ⊔ g) = limsup u f ⊔ limsup u g.
Русский
Для любого фильтра f на β выполняется: limsup u (f ⊔ g) = limsup u f ⊔ limsup u g.
LaTeX
$$$\\operatorname{limsup} u (f \\sqcup g) = \\operatorname{limsup} u f \\sqcup \\operatorname{limsup} u g$$$
Lean4
theorem limsup_sup_filter {g} : limsup u (f ⊔ g) = limsup u f ⊔ limsup u g :=
by
refine le_antisymm ?_ (sup_le (limsup_le_limsup_of_le le_sup_left) (limsup_le_limsup_of_le le_sup_right))
simp_rw [limsup_eq, sInf_sup_eq, sup_sInf_eq, mem_setOf_eq, le_iInf₂_iff]
intro a ha b hb
exact sInf_le ⟨ha.mono fun _ h ↦ h.trans le_sup_left, hb.mono fun _ h ↦ h.trans le_sup_right⟩
