Theorems · Theorem · order theory

Filter.HasBasis.limsup_eq_ite

∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLinearOrder α] {v : Filter ι}
  {p : ι' → Prop} {s : ι' → Set ι} [inst_1 : Countable (Subtype p)] [inst_2 : Nonempty (Subtype p)],
  v.HasBasis p s →
    ∀ (f : ι → α),
      Filter.limsup f v =
        if ∃ j, s ↑j = ∅ then sInf Set.univ
        else if ∀ (j : Subtype p), ¬BddAbove (Set.range fun i => f ↑i) then sInf ∅ else ⨅ j, ⨆ i, f ↑i

Writing a limsup as an infimum of supremum, in a (possibly non-complete) conditionally complete linear order. A reparametrization trick is needed to avoid taking the supremum of sets which are not bounded below.

Defined in

Mathlib.Order.LiminfLimsup

Cited by

0 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderCountableNonempty