Commit 2022-02-15 15:52 9307f5b4

feat(topology/order/lattice): add a consequence of the continuity of sup/inf (#12003) Prove this lemma and its inf counterpart:

lemma filter.tendsto.sup_right_nhds {ι β} [topological_space β] [has_sup β] [has_continuous_sup β]
  {l : filter ι} {f g : ι → β} {x y : β} (hf : tendsto f l (𝓝 x)) (hg : tendsto g l (𝓝 y)) :
  tendsto (f ⊔ g) l (𝓝 (x ⊔ y))

The name is sup_right_nhds because sup already exists, and is about a supremum over the filters on the left in the tendsto. The proofs of tendsto_prod_iff' and prod.tendsto_iff were written by Patrick Massot.