∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] [Nonempty ι] {f : ι → α},
  Directed (fun x1 x2 => x2 ≤ x1) f → BddBelow (Set.range f) → Set.Iic (⨅ i, f i) = ⋂ i, Set.Iic (f i)