∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedAddCommGroup G] [inst_3 : Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G}
  {f : α → G},
  (∀ (i : ι), Continuous (F i)) →
    Antitone F →
      Continuous f →
        (∀ (x : α), Filter.Tendsto (fun x_1 => F x_1 x) Filter.atTop (nhds (f x))) →
          TendstoLocallyUniformly F f Filter.atTop