mathlib

9307f5b4 - feat(topology/order/lattice): add a consequence of the continuity of sup/inf (#12003)

feat(topology/order/lattice): add a consequence of the continuity of sup/inf (#12003) Prove this lemma and its `inf` counterpart: ```lean 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. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>