Theorems · Theorem · order theory

Filter.liminf_le_limsup_of_frequently_le

∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β},
  (∃ᶠ (x : α) in f, u x ≤ v x) →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.liminf_le_limsup_of_frequently_le._auto_1 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) Filter.liminf_le_limsup_of_frequently_le._auto_3 →
        Filter.liminf u f ≤ Filter.limsup v f

Defined in

Mathlib.Order.LiminfLimsup

Cited by

2 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrder