∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α] [inst_2 : CompleteLattice α]
  [InfConvergenceClass α] {f : ι → α}, Antitone f → Filter.Tendsto f Filter.atTop (nhds (⨅ i, f i))