∀ {α : Type u} {β : Type v} {ι : Sort x} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [Nonempty ι] {f : α → β},
  LeftOrdContinuous f → ∀ {g : ι → α}, BddAbove (Set.range g) → f (⨆ i, g i) = ⨆ i, f (g i)