∀ {L : Type u_1} [inst : TopologicalSpace L] {α : Type u_3} {l : Filter α} {f g : α → L} {x y : L} [inst_1 : Min L]
  [ContinuousInf L],
  Filter.Tendsto f l (nhds x) → Filter.Tendsto g l (nhds y) → Filter.Tendsto (fun i => f i ⊓ g i) l (nhds (x ⊓ y))