∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_6} {ι' : Type u_7} {f : ι → α} {v : Filter ι}
  {p : ι' → Prop} {s : ι' → Set ι}, v.HasBasis p s → Filter.liminf f v = sSup (⋃ j, ⋂ i, Set.Iic (f ↑i))