English
For a set s ⊆ β, function u, and values v, the limsup of the piecewise combination equals the max of the two limsups corresponding to membership and non-membership in s.
Русский
Для множества s и функций u, v равенство лимсупа разбиения по s дает максимум между двумя частями по членству в s и нечленству.
LaTeX
$$$\\operatorname{limsup}(s.{\\text{piecewise}}\\,u\,v) = \\operatorname{blimsup} u f (\\cdot \\in s) \\; \\sqcup \\; \\operatorname{blimsup} v f (\\cdot \\notin s)$$$
Lean4
theorem limsup_piecewise {s : Set β} [DecidablePred (· ∈ s)] {v} :
limsup (s.piecewise u v) f = blimsup u f (· ∈ s) ⊔ blimsup v f (· ∉ s) :=
by
rw [← blimsup_sup_not (p := (· ∈ s))]
refine congr_arg₂ _ (blimsup_congr ?_) (blimsup_congr ?_) <;> filter_upwards with _ h using by simp [h]
