Theorems · Theorem · order theory

Filter.limsup_piecewise

∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {u : β → α} {s : Set β}
  [inst_1 : DecidablePred fun x => x ∈ s] {v : β → α},
  Filter.limsup (s.piecewise u v) f = (Filter.blimsup u f fun x => x ∈ s) ⊔ Filter.blimsup v f fun x => x ∉ s

Defined in

Mathlib.Order.LiminfLimsup

Cited by

2 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteDistribLatticeDecidablePred