∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [Nonempty ι] (e : α ≃o β) {f : ι → α},
  BddBelow (Set.range f) → e (⨅ i, f i) = ⨅ i, e (f i)