feat(Topology): add IsCompact.nhdsSet_prod_eq etc (#6961)

Also delete `NhdsContainBoxes` and related lemmas as they were only used for another proof of `generalized_tube_lemma`.

Author: urkud

Mathlib/Topology/SubsetProperties.lean

@@ -220,9 +220,8 @@ theorem IsCompact.disjoint_nhdsSet_left {l : Filter α} (hs : IsCompact s) :
   choose! U hxU hUl using fun x hx => (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)
   choose hxU hUo using hxU
   rcases hs.elim_nhds_subcover U fun x hx => (hUo x hx).mem_nhds (hxU x hx) with ⟨t, hts, hst⟩
-  refine'
-    (hasBasis_nhdsSet _).disjoint_iff_left.2
-      ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx => hUo x (hts x hx), hst⟩, _⟩
+  refine (hasBasis_nhdsSet _).disjoint_iff_left.2
+    ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx => hUo x (hts x hx), hst⟩, ?_⟩
   rw [compl_iUnion₂, biInter_finset_mem]
   exact fun x hx => hUl x (hts x hx)
 #align is_compact.disjoint_nhds_set_left IsCompact.disjoint_nhdsSet_left
@@ -369,26 +368,47 @@ theorem isCompact_iff_finite_subfamily_closed :
   ⟨fun hs => hs.elim_finite_subfamily_closed, isCompact_of_finite_subfamily_closed⟩
 #align is_compact_iff_finite_subfamily_closed isCompact_iff_finite_subfamily_closed
 
+/-- If `s : Set (α × β)` belongs to `𝓝 x ×ˢ l` for all `x` from a compact set `K`,
+then it belongs to `(𝓝ˢ K) ×ˢ l`,
+i.e., there exist an open `U ⊇ K` and `t ∈ l` such that `U ×ˢ t ⊆ s`. -/
+theorem IsCompact.mem_nhdsSet_prod_of_forall {K : Set α} {l : Filter β} {s : Set (α × β)}
+    (hK : IsCompact K) (hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l) : s ∈ (𝓝ˢ K) ×ˢ l := by
+  refine hK.induction_on (by simp) (fun t t' ht hs ↦ ?_) (fun t t' ht ht' ↦ ?_) fun x hx ↦ ?_
+  · exact prod_mono (nhdsSet_mono ht) le_rfl hs
+  · simp [sup_prod, *]
+  · rcases ((nhds_basis_opens _).prod l.basis_sets).mem_iff.1 (hs x hx)
+      with ⟨⟨u, v⟩, ⟨⟨hx, huo⟩, hv⟩, hs⟩
+    refine ⟨u, nhdsWithin_le_nhds (huo.mem_nhds hx), mem_of_superset ?_ hs⟩
+    exact prod_mem_prod (huo.mem_nhdsSet.2 Subset.rfl) hv
+
+theorem IsCompact.nhdsSet_prod_eq_biSup {K : Set α} (hK : IsCompact K) (l : Filter β) :
+    (𝓝ˢ K) ×ˢ l = ⨆ x ∈ K, 𝓝 x ×ˢ l :=
+  le_antisymm (fun s hs ↦ hK.mem_nhdsSet_prod_of_forall <| by simpa using hs)
+    (iSup₂_le fun x hx ↦ prod_mono (nhds_le_nhdsSet hx) le_rfl)
+
+theorem IsCompact.prod_nhdsSet_eq_biSup {K : Set β} (hK : IsCompact K) (l : Filter α) :
+    l ×ˢ (𝓝ˢ K) = ⨆ y ∈ K, l ×ˢ 𝓝 y := by
+  simp only [prod_comm (f := l), hK.nhdsSet_prod_eq_biSup, map_iSup]
+
+/-- If `s : Set (α × β)` belongs to `l ×ˢ 𝓝 y` for all `y` from a compact set `K`,
+then it belongs to `l ×ˢ (𝓝ˢ K)`,
+i.e., there exist `t ∈ l` and an open `U ⊇ K` such that `t ×ˢ U ⊆ s`. -/
+theorem IsCompact.mem_prod_nhdsSet_of_forall {K : Set β} {l : Filter α} {s : Set (α × β)}
+    (hK : IsCompact K) (hs : ∀ y ∈ K, s ∈ l ×ˢ 𝓝 y) : s ∈ l ×ˢ 𝓝ˢ K :=
+  (hK.prod_nhdsSet_eq_biSup l).symm ▸ by simpa using hs
+
 /-- To show that `∀ y ∈ K, P x y` holds for `x` close enough to `x₀` when `K` is compact,
 it is sufficient to show that for all `y₀ ∈ K` there `P x y` holds for `(x, y)` close enough
 to `(x₀, y₀)`.
+
+Provided for backwards compatibility,
+see `IsCompact.mem_prod_nhdsSet_of_forall` for a stronger statement.
 -/
 theorem IsCompact.eventually_forall_of_forall_eventually {x₀ : α} {K : Set β} (hK : IsCompact K)
     {P : α → β → Prop} (hP : ∀ y ∈ K, ∀ᶠ z : α × β in 𝓝 (x₀, y), P z.1 z.2) :
     ∀ᶠ x in 𝓝 x₀, ∀ y ∈ K, P x y := by
-  refine' hK.induction_on _ _ _ _
-  · exact eventually_of_forall fun x y => False.elim
-  · intro s t hst ht
-    refine' ht.mono fun x h y hys => h y <| hst hys
-  · intro s t hs ht
-    filter_upwards [hs, ht]
-    rintro x h1 h2 y (hys | hyt)
-    exacts [h1 y hys, h2 y hyt]
-  · intro y hyK
-    specialize hP y hyK
-    rw [nhds_prod_eq, eventually_prod_iff] at hP
-    rcases hP with ⟨p, hp, q, hq, hpq⟩
-    exact ⟨{ y | q y }, mem_nhdsWithin_of_mem_nhds hq, eventually_of_mem hp @hpq⟩
+  simp only [nhds_prod_eq, ← eventually_iSup, ← hK.prod_nhdsSet_eq_biSup] at hP
+  exact hP.curry.mono fun _ h ↦ h.self_of_nhdsSet
 #align is_compact.eventually_forall_of_forall_eventually IsCompact.eventually_forall_of_forall_eventually
 
 @[simp]
@@ -640,71 +660,40 @@ theorem inCompact.isBounded_iff : @IsBounded _ (inCompact α) s ↔ ∃ t, IsCom
 
 end Bornology
 
-section TubeLemma
-
-/-- `NhdsContainBoxes s t` means that any open neighborhood of `s × t` in `α × β` includes
-a product of an open neighborhood of `s` by an open neighborhood of `t`. -/
-def NhdsContainBoxes (s : Set α) (t : Set β) : Prop :=
-  ∀ n : Set (α × β), IsOpen n → (s ×ˢ t ⊆ n) →
-    ∃ (u : Set α) (v : Set β), IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
-#align nhds_contain_boxes NhdsContainBoxes
-
-@[symm]
-theorem NhdsContainBoxes.symm {s : Set α} {t : Set β} :
-    NhdsContainBoxes s t → NhdsContainBoxes t s := fun H n hn hp =>
-  let ⟨u, v, uo, vo, su, tv, p⟩ :=
-    H (Prod.swap ⁻¹' n) (hn.preimage continuous_swap) (by rwa [← image_subset_iff, image_swap_prod])
-  ⟨v, u, vo, uo, tv, su, by rwa [← image_subset_iff, image_swap_prod] at p⟩
-#align nhds_contain_boxes.symm NhdsContainBoxes.symm
-
-theorem NhdsContainBoxes.comm {s : Set α} {t : Set β} :
-    NhdsContainBoxes s t ↔ NhdsContainBoxes t s :=
-  Iff.intro NhdsContainBoxes.symm NhdsContainBoxes.symm
-#align nhds_contain_boxes.comm NhdsContainBoxes.comm
-
-theorem nhdsContainBoxes_of_singleton {x : α} {y : β} :
-    NhdsContainBoxes ({x} : Set α) ({y} : Set β) := fun n hn hp =>
-  let ⟨u, v, uo, vo, xu, yv, hp'⟩ := isOpen_prod_iff.mp hn x y (hp <| by simp)
-  ⟨u, v, uo, vo, by simpa, by simpa, hp'⟩
-#align nhds_contain_boxes_of_singleton nhdsContainBoxes_of_singleton
-
-theorem nhdsContainBoxes_of_compact {s : Set α} (hs : IsCompact s) (t : Set β)
-    (H : ∀ x ∈ s, NhdsContainBoxes ({x} : Set α) t) : NhdsContainBoxes s t := fun n hn hp =>
-  have :
-    ∀ x : s,
-      ∃ uv : Set α × Set β, IsOpen uv.1 ∧ IsOpen uv.2 ∧ {↑x} ⊆ uv.1 ∧ t ⊆ uv.2 ∧ uv.1 ×ˢ uv.2 ⊆ n :=
-    fun ⟨x, hx⟩ =>
-    have : ({x} : Set α) ×ˢ t ⊆ n := Subset.trans (prod_mono (by simpa) Subset.rfl) hp
-    let ⟨ux, vx, H1⟩ := H x hx n hn this
-    ⟨⟨ux, vx⟩, H1⟩
-  let ⟨uvs, h⟩ := Classical.axiom_of_choice this
-  have us_cover : s ⊆ ⋃ i, (uvs i).1 := fun x hx =>
-    subset_iUnion _ ⟨x, hx⟩ (by simpa using (h ⟨x, hx⟩).2.2.1)
-  let ⟨s0, s0_cover⟩ := hs.elim_finite_subcover _ (fun i => (h i).1) us_cover
-  let u := ⋃ i ∈ s0, (uvs i).1
-  let v := ⋂ i ∈ s0, (uvs i).2
-  have : IsOpen u := isOpen_biUnion fun i _ => (h i).1
-  have : IsOpen v := isOpen_biInter s0.finite_toSet fun i _ => (h i).2.1
-  have : t ⊆ v := subset_iInter₂ fun i _ => (h i).2.2.2.1
-  have : u ×ˢ v ⊆ n := fun ⟨x', y'⟩ ⟨hx', hy'⟩ =>
-    have : ∃ i ∈ s0, x' ∈ (uvs i).1 := by simpa using hx'
-    let ⟨i, is0, hi⟩ := this
-    (h i).2.2.2.2 ⟨hi, (biInter_subset_of_mem is0 : v ⊆ (uvs i).2) hy'⟩
-  ⟨u, v, ‹IsOpen u›, ‹IsOpen v›, s0_cover, ‹t ⊆ v›, ‹u ×ˢ v ⊆ n›⟩
-#align nhds_contain_boxes_of_compact nhdsContainBoxes_of_compact
+#noalign nhds_contain_boxes
+#noalign nhds_contain_boxes.symm
+#noalign nhds_contain_boxes.comm
+#noalign nhds_contain_boxes_of_singleton
+#noalign nhds_contain_boxes_of_compact
+
+/-- If `s` and `t` are compact sets, then the set neighborhoods filter of `s ×ˢ t`
+is the product of set neighborhoods filters for `s` and `t`.
+
+For general sets, only the `≤` inequality holds, see `nhdsSet_prod_le`. -/
+theorem IsCompact.nhdsSet_prod_eq {s : Set α} {t : Set β} (hs : IsCompact s) (ht : IsCompact t) :
+    𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t := by
+  simp_rw [hs.nhdsSet_prod_eq_biSup, ht.prod_nhdsSet_eq_biSup, nhdsSet, sSup_image, biSup_prod,
+    nhds_prod_eq]
+
+/-- The product of a neighborhood of `s` and a neighborhood of `t` is a neighborhood of `s ×ˢ t`,
+formulated in terms of a filter inequality. -/
+theorem nhdsSet_prod_le (s : Set α) (t : Set β) : 𝓝ˢ (s ×ˢ t) ≤ 𝓝ˢ s ×ˢ 𝓝ˢ t :=
+  ((hasBasis_nhdsSet _).prod (hasBasis_nhdsSet _)).ge_iff.2 fun (_u, _v) ⟨⟨huo, hsu⟩, hvo, htv⟩ ↦
+    (huo.prod hvo).mem_nhdsSet.2 <| prod_mono hsu htv
 
 /-- If `s` and `t` are compact sets and `n` is an open neighborhood of `s × t`, then there exist
-open neighborhoods `u ⊇ s` and `v ⊇ t` such that `u × v ⊆ n`. -/
+open neighborhoods `u ⊇ s` and `v ⊇ t` such that `u × v ⊆ n`.
+
+See also `IsCompact.nhdsSet_prod_eq`. -/
 theorem generalized_tube_lemma {s : Set α} (hs : IsCompact s) {t : Set β} (ht : IsCompact t)
     {n : Set (α × β)} (hn : IsOpen n) (hp : s ×ˢ t ⊆ n) :
-    ∃ (u : Set α) (v : Set β), IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n :=
-  have := nhdsContainBoxes_of_compact hs t fun x _ => NhdsContainBoxes.symm <|
-    nhdsContainBoxes_of_compact ht {x} fun _ _ => nhdsContainBoxes_of_singleton
-  this n hn hp
+    ∃ (u : Set α) (v : Set β), IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n := by
+  rw [← hn.mem_nhdsSet, hs.nhdsSet_prod_eq ht,
+    ((hasBasis_nhdsSet _).prod (hasBasis_nhdsSet _)).mem_iff] at hp
+  rcases hp with ⟨⟨u, v⟩, ⟨⟨huo, hsu⟩, hvo, htv⟩, hn⟩
+  exact ⟨u, v, huo, hvo, hsu, htv, hn⟩
 #align generalized_tube_lemma generalized_tube_lemma
 
-end TubeLemma
-
 /-- Type class for compact spaces. Separation is sometimes included in the definition, especially
 in the French literature, but we do not include it here. -/
 class CompactSpace (α : Type*) [TopologicalSpace α] : Prop where