Theorems · Theorem · order theory

Filter.HasBasis.liminf_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.liminf f v =
        if ∃ j, s ↑j = ∅ then sSup Set.univ
        else if ∀ (j : Subtype p), ¬BddBelow (Set.range fun i => f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i

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

Defined in

Mathlib.Order.LiminfLimsup

Cited by

2 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderCountableNonempty