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>

src/order/filter/basic.lean

@@ -2666,6 +2666,11 @@ lemma tendsto_prod_iff {f : α × β → γ} {x : filter α} {y : filter β} {z
   ∀ W ∈ z, ∃ U ∈ x,  ∃ V ∈ y, ∀ x y, x ∈ U → y ∈ V → f (x, y) ∈ W :=
 by simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff, exists_prop, iff_self]
 
+lemma tendsto_prod_iff' {f : filter α} {g : filter β} {g' : filter γ}
+  {s : α → β × γ} :
+  tendsto s f (g ×ᶠ g') ↔ tendsto (λ n, (s n).1) f g ∧ tendsto (λ n, (s n).2) f g' :=
+by { unfold filter.prod, simp only [tendsto_inf, tendsto_comap_iff, iff_self] }
+
 end prod
 
 /-! ### Coproducts of filters -/

src/topology/constructions.lean

@@ -301,6 +301,11 @@ begin
     exact ⟨u, u_open.mem_nhds au, v, v_open.mem_nhds bv, huv⟩ }
 end
 
+lemma _root_.prod.tendsto_iff {α} (seq : α → β × γ) {f : filter α} (x : β × γ) :
+  tendsto seq f (𝓝 x)
+    ↔ tendsto (λ n, (seq n).fst) f (𝓝 x.fst) ∧ tendsto (λ n, (seq n).snd) f (𝓝 x.snd) :=
+by { cases x, rw [nhds_prod_eq, filter.tendsto_prod_iff'], }
+
 lemma filter.has_basis.prod_nhds {ιa ιb : Type*} {pa : ιa → Prop} {pb : ιb → Prop}
   {sa : ιa → set α} {sb : ιb → set β} {a : α} {b : β} (ha : (𝓝 a).has_basis pa sa)
   (hb : (𝓝 b).has_basis pb sb) :

src/topology/order/lattice.lean

@@ -22,6 +22,9 @@ and `has_continuous_sup`.
 topological, lattice
 -/
 
+open filter
+open_locale topological_space
+
 /--
 Let `L` be a topological space and let `L×L` be equipped with the product topology and let
 `⊓:L×L → L` be an infimum. Then `L` is said to have *(jointly) continuous infimum* if the map
@@ -82,3 +85,27 @@ has_continuous_sup.continuous_sup
   {f g : X → L} (hf : continuous f) (hg : continuous g) :
   continuous (λx, f x ⊔ g x) :=
 continuous_sup.comp (hf.prod_mk hg : _)
+
+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)) :=
+(continuous_sup.tendsto _).comp (tendsto.prod_mk_nhds hf hg)
+
+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 (λ i, f i ⊔ g i) l (𝓝 (x ⊔ y)) :=
+hf.sup_right_nhds' hg
+
+lemma filter.tendsto.inf_right_nhds' {ι β} [topological_space β] [has_inf β] [has_continuous_inf β]
+  {l : filter ι} {f g : ι → β} {x y : β}
+  (hf : tendsto f l (𝓝 x)) (hg : tendsto g l (𝓝 y)) :
+  tendsto (f ⊓ g) l (𝓝 (x ⊓ y)) :=
+(continuous_inf.tendsto _).comp (tendsto.prod_mk_nhds hf hg)
+
+lemma filter.tendsto.inf_right_nhds {ι β} [topological_space β] [has_inf β] [has_continuous_inf β]
+  {l : filter ι} {f g : ι → β} {x y : β}
+  (hf : tendsto f l (𝓝 x)) (hg : tendsto g l (𝓝 y)) :
+  tendsto (λ i, f i ⊓ g i) l (𝓝 (x ⊓ y)) :=
+hf.inf_right_nhds' hg