Theorems · Theorem · order theory

Filter.limsup_comp

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α] (u : β → α) (v : γ → β)
  (f : Filter γ), Filter.limsup (u ∘ v) f = Filter.limsup u (Filter.map v f)

Defined in

Mathlib.Order.LiminfLimsup

Cited by

2 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

ConditionallyCompleteLattice