∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} {f : α → β}
  {g : ι → α}, ContinuousAt f (iInf g) → Monotone f → f ⊤ = ⊤ → f (iInf g) = iInf (f ∘ g)