Theorems · Theorem · general topology

le_limsup_add

∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommGroup α] [inst_1 : ConditionallyCompleteLinearOrder α] [DenselyOrdered α]
  [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) le_limsup_add._auto_1 →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) le_limsup_add._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) le_limsup_add._auto_5 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) le_limsup_add._auto_7 →
          Filter.limsup u f + Filter.liminf v f ≤ Filter.limsup (u + v) f

Defined in

Mathlib.Topology.Algebra.Order.LiminfLimsup

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupConditionallyCompleteLinearOrderDenselyOrderedAddLeftMonoFilter.NeBot