From 3d7c3c86b90b47b762b72b361ede5fe789f7f5af Mon Sep 17 00:00:00 2001
From: Winston Yin <winstonyin@gmail.com>
Date: Mon, 10 Feb 2025 07:27:03 +0000
Subject: [PATCH] feat(Topology/EMetricSpace/Lipschitz): add lemmas with
 swapped arguments (#20696)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The existing series of lemmas on the continuity of `f : α × β → γ` requires Lipschitz continuity in `α` and continuity in `β`. I add a series of mirror lemmas with the argument positions swapped, i.e. continuity in `α` and Lipschitz continuity in `β`. This improves usability, for example, in the Picard-Lindelöf theorem, where the time-dependent vector field is typically assumed to be continuous in time (the first component) and Lipschitz continuous in space (the second component).
---
 Mathlib/Data/Set/Prod.lean                   |  3 ++
 Mathlib/Topology/EMetricSpace/Lipschitz.lean | 34 +++++++++++++++++++-
 2 files changed, 36 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Set/Prod.lean b/Mathlib/Data/Set/Prod.lean
index 742054186e40a..2279be7fcf405 100644
--- a/Mathlib/Data/Set/Prod.lean
+++ b/Mathlib/Data/Set/Prod.lean
@@ -232,6 +232,9 @@ theorem preimage_swap_prod (s : Set α) (t : Set β) : Prod.swap ⁻¹' s ×ˢ t
 theorem image_swap_prod (s : Set α) (t : Set β) : Prod.swap '' s ×ˢ t = t ×ˢ s := by
   rw [image_swap_eq_preimage_swap, preimage_swap_prod]
 
+theorem mapsTo_swap_prod (s : Set α) (t : Set β) : MapsTo Prod.swap (s ×ˢ t) (t ×ˢ s) :=
+  fun _ ⟨hx, hy⟩ ↦ ⟨hy, hx⟩
+
 theorem prod_image_image_eq {m₁ : α → γ} {m₂ : β → δ} :
     (m₁ '' s) ×ˢ (m₂ '' t) = (fun p : α × β => (m₁ p.1, m₂ p.2)) '' s ×ˢ t :=
   ext <| by
diff --git a/Mathlib/Topology/EMetricSpace/Lipschitz.lean b/Mathlib/Topology/EMetricSpace/Lipschitz.lean
index 18d504702f609..7bdac4c8e1f3b 100644
--- a/Mathlib/Topology/EMetricSpace/Lipschitz.lean
+++ b/Mathlib/Topology/EMetricSpace/Lipschitz.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2018 Rohan Mitta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rohan Mitta, Kevin Buzzard, Alistair Tucker, Johannes Hölzl, Yury Kudryashov
+Authors: Rohan Mitta, Kevin Buzzard, Alistair Tucker, Johannes Hölzl, Yury Kudryashov, Winston Yin
 -/
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Topology.EMetricSpace.Diam
@@ -476,3 +476,35 @@ theorem continuous_prod_of_continuous_lipschitzWith [PseudoEMetricSpace α] [Top
     [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) (ha : ∀ a, Continuous fun y => f (a, y))
     (hb : ∀ b, LipschitzWith K fun x => f (x, b)) : Continuous f :=
   continuous_prod_of_dense_continuous_lipschitzWith f K dense_univ (fun _ _ ↦ ha _) hb
+
+theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith' [TopologicalSpace α]
+    [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t t' : Set β}
+    (ht' : t' ⊆ t) (htt' : t ⊆ closure t') (K : ℝ≥0)
+    (ha : ∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t)
+    (hb : ∀ b ∈ t', ContinuousOn (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t) :=
+  have : ContinuousOn (f ∘ Prod.swap) (t ×ˢ s) :=
+    continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith _ ht' htt' K hb ha
+  this.comp continuous_swap.continuousOn (mapsTo_swap_prod _ _)
+
+theorem continuousOn_prod_of_continuousOn_lipschitzOnWith' [TopologicalSpace α]
+    [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : ℝ≥0)
+    (ha : ∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t)
+    (hb : ∀ b ∈ t, ContinuousOn (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t) :=
+  have : ContinuousOn (f ∘ Prod.swap) (t ×ˢ s) :=
+    continuousOn_prod_of_continuousOn_lipschitzOnWith _ K hb ha
+  this.comp continuous_swap.continuousOn (mapsTo_swap_prod _ _)
+
+theorem continuous_prod_of_dense_continuous_lipschitzWith' [TopologicalSpace α]
+    [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) {t : Set β}
+    (ht : Dense t) (ha : ∀ a, LipschitzWith K fun y => f (a, y))
+    (hb : ∀ b ∈ t, Continuous fun x => f (x, b)) : Continuous f :=
+  have : Continuous (f ∘ Prod.swap) :=
+    continuous_prod_of_dense_continuous_lipschitzWith _ K ht hb ha
+  this.comp continuous_swap
+
+theorem continuous_prod_of_continuous_lipschitzWith' [TopologicalSpace α] [PseudoEMetricSpace β]
+    [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) (ha : ∀ a, LipschitzWith K fun y => f (a, y))
+    (hb : ∀ b, Continuous fun x => f (x, b)) : Continuous f :=
+  have : Continuous (f ∘ Prod.swap) :=
+    continuous_prod_of_continuous_lipschitzWith _ K hb ha
+  this.comp continuous_swap