∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f : β → α}
  {l : Filter β} {a : α},
  Filter.Tendsto f l (nhdsWithin a (Set.Ioi a)) → Filter.Tendsto (fun i => max (f i) a) l (nhdsWithin a (Set.Ioi a))