Theorems · Theorem · order theory

Filter.Tendsto.limsup_comp_le_limsup

∀ {ι : Type u_6} {α : Type u_7} {β : Type u_8} [inst : ConditionallyCompleteLattice β] {v : ι → α} {u : α → β}
  {f : Filter ι} {g : Filter α},
  Filter.Tendsto v f g →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (Filter.map v f) u)
        Filter.Tendsto.limsup_comp_le_limsup._auto_1 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) g u) Filter.Tendsto.limsup_comp_le_limsup._auto_3 →
        Filter.limsup (u ∘ v) f ≤ Filter.limsup u g

Defined in

Mathlib.Order.LiminfLimsup

Cited by

1 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLattice