chore(topology/*): use dot notation for is_open.prod and `is_closed…

….prod` (#4510)

src/analysis/calculus/deriv.lean

@@ -1218,7 +1218,7 @@ begin
   suffices : is_o (λ p : 𝕜 × 𝕜, (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹))
     (λ (p : 𝕜 × 𝕜), (p.1 - p.2) * 1) (𝓝 (x, x)),
   { refine this.congr' _ (eventually_of_forall $ λ _, mul_one _),
-    refine eventually.mono (mem_nhds_sets (is_open_prod is_open_ne is_open_ne) ⟨hx, hx⟩) _,
+    refine eventually.mono (mem_nhds_sets (is_open_ne.prod is_open_ne) ⟨hx, hx⟩) _,
     rintro ⟨y, z⟩ ⟨hy, hz⟩,
     simp only [mem_set_of_eq] at hy hz, -- hy : y ≠ 0, hz : z ≠ 0
     field_simp [hx, hy, hz], ring, },

src/analysis/special_functions/pow.lean

@@ -431,12 +431,12 @@ begin
   cases lt_trichotomy 0 x,
   exact continuous_within_at.continuous_at
     (continuous_on_iff_continuous_restrict.2 continuous_rpow_aux1 _ h)
-    (mem_nhds_sets (by { convert is_open_prod (is_open_lt' (0:ℝ)) is_open_univ, ext, finish }) h),
+    (mem_nhds_sets (by { convert (is_open_lt' (0:ℝ)).prod is_open_univ, ext, finish }) h),
   cases h,
   { exact absurd h.symm hx },
   exact continuous_within_at.continuous_at
     (continuous_on_iff_continuous_restrict.2 continuous_rpow_aux2 _ h)
-    (mem_nhds_sets (by { convert is_open_prod (is_open_gt' (0:ℝ)) is_open_univ, ext, finish }) h)
+    (mem_nhds_sets (by { convert (is_open_gt' (0:ℝ)).prod is_open_univ, ext, finish }) h)
 end
 
 lemma continuous_rpow_aux3 : continuous (λ p : {p:ℝ×ℝ // 0 < p.2}, p.val.1 ^ p.val.2) :=
@@ -472,7 +472,7 @@ lemma continuous_at_rpow_of_pos (hy : 0 < y) (x : ℝ) :
   continuous_at (λp:ℝ×ℝ, p.1^p.2) (x, y) :=
 continuous_within_at.continuous_at
   (continuous_on_iff_continuous_restrict.2 continuous_rpow_aux3 _ hy)
-  (mem_nhds_sets (by { convert is_open_prod is_open_univ (is_open_lt' (0:ℝ)), ext, finish }) hy)
+  (mem_nhds_sets (by { convert is_open_univ.prod (is_open_lt' (0:ℝ)), ext, finish }) hy)
 
 lemma continuous_at_rpow {x y : ℝ} (h : x ≠ 0 ∨ 0 < y) :
   continuous_at (λp:ℝ×ℝ, p.1^p.2) (x, y) :=

src/topology/algebra/open_subgroup.lean

@@ -111,7 +111,7 @@ variables {H : Type*} [group H] [topological_space H]
 @[to_additive "The product of two open subgroups as an open subgroup of the product group."]
 def prod (U : open_subgroup G) (V : open_subgroup H) : open_subgroup (G × H) :=
 { carrier := (U : set G).prod (V : set H),
-  is_open' := is_open_prod U.is_open V.is_open,
+  is_open' := U.is_open.prod V.is_open,
   .. (U : subgroup G).prod (V : subgroup H) }
 
 end

src/topology/compact_open.lean

@@ -71,7 +71,7 @@ continuous_iff_continuous_at.mpr $ assume ⟨f, x⟩ n hn,
     f' x' ∈ f' '' s  : mem_image_of_mem f' (us hx')
     ...       ⊆ v            : hf'
     ...       ⊆ n            : vn,
-  have is_open w, from is_open_prod (is_open_gen sc vo) uo,
+  have is_open w, from (is_open_gen sc vo).prod uo,
   have (f, x) ∈ w, from ⟨image_subset_iff.mpr sv, xu⟩,
   mem_nhds_sets_iff.mpr ⟨w, by assumption, by assumption, by assumption⟩
 

src/topology/constructions.lean

@@ -150,7 +150,7 @@ lemma filter.eventually.prod_mk_nhds {pa : α → Prop} {a} (ha : ∀ᶠ x in 
 lemma continuous_swap : continuous (prod.swap : α × β → β × α) :=
 continuous.prod_mk continuous_snd continuous_fst
 
-lemma is_open_prod {s : set α} {t : set β} (hs : is_open s) (ht : is_open t) :
+lemma is_open.prod {s : set α} {t : set β} (hs : is_open s) (ht : is_open t) :
   is_open (set.prod s t) :=
 is_open_inter (continuous_fst s hs) (continuous_snd t ht)
 
@@ -200,7 +200,7 @@ lemma prod_generate_from_generate_from_eq {α : Type*} {β : Type*} {s : set (se
 let G := generate_from {g | ∃u∈s, ∃v∈t, g = set.prod u v} in
 le_antisymm
   (le_generate_from $ assume g ⟨u, hu, v, hv, g_eq⟩, g_eq.symm ▸
-    @is_open_prod _ _ (generate_from s) (generate_from t) _ _
+    @is_open.prod _ _ (generate_from s) (generate_from t) _ _
       (generate_open.basic _ hu) (generate_open.basic _ hv))
   (le_inf
     (coinduced_le_iff_le_induced.mp $ le_generate_from $ assume u hu,
@@ -224,7 +224,7 @@ lemma prod_eq_generate_from :
   prod.topological_space =
   generate_from {g | ∃(s:set α) (t:set β), is_open s ∧ is_open t ∧ g = set.prod s t} :=
 le_antisymm
-  (le_generate_from $ assume g ⟨s, t, hs, ht, g_eq⟩, g_eq.symm ▸ is_open_prod hs ht)
+  (le_generate_from $ assume g ⟨s, t, hs, ht, g_eq⟩, g_eq.symm ▸ hs.prod ht)
   (le_inf
     (ball_image_of_ball $ λt ht, generate_open.basic _ ⟨t, univ, by simpa [set.prod_eq] using ht⟩)
     (ball_image_of_ball $ λt ht, generate_open.basic _ ⟨univ, t, by simpa [set.prod_eq] using ht⟩))
@@ -308,7 +308,7 @@ begin
         exact is_open_map_snd _ H } },
     { assume H,
       simp [st.1.ne_empty, st.2.ne_empty] at H,
-      exact is_open_prod H.1 H.2 } }
+      exact H.1.prod H.2 } }
 end
 
 lemma closure_prod_eq {s : set α} {t : set β} :
@@ -326,7 +326,7 @@ have (a, b) ∈ closure (set.prod s t), by rw [closure_prod_eq]; from ⟨ha, hb
 show (λp:α×β, f p.1 p.2) (a, b) ∈ closure u, from
   mem_closure hf this $ assume ⟨a, b⟩ ⟨ha, hb⟩, hu a b ha hb
 
-lemma is_closed_prod {s₁ : set α} {s₂ : set β} (h₁ : is_closed s₁) (h₂ : is_closed s₂) :
+lemma is_closed.prod {s₁ : set α} {s₂ : set β} (h₁ : is_closed s₁) (h₂ : is_closed s₂) :
   is_closed (set.prod s₁ s₂) :=
 closure_eq_iff_is_closed.mp $ by simp only [h₁.closure_eq, h₂.closure_eq, closure_prod_eq]
 

src/topology/instances/complex.lean

@@ -91,8 +91,7 @@ tendsto_of_uniform_continuous_subtype
     ({x | abs x < abs a₁ + 1}.prod {x | abs x < abs a₂ + 1})
     (λ x, id))
   (mem_nhds_sets
-    (is_open_prod
-      (continuous_abs _ $ is_open_gt' (abs a₁ + 1))
+    ((continuous_abs _ $ is_open_gt' (abs a₁ + 1)).prod
       (continuous_abs _ $ is_open_gt' (abs a₂ + 1)))
     ⟨lt_add_one (abs a₁), lt_add_one (abs a₂)⟩)
 

src/topology/instances/real.lean

@@ -188,8 +188,7 @@ tendsto_of_uniform_continuous_subtype
     ({x | abs x < abs a₁ + 1}.prod {x | abs x < abs a₂ + 1})
     (λ x, id))
   (mem_nhds_sets
-    (is_open_prod
-      (real.continuous_abs _ $ is_open_gt' (abs a₁ + 1))
+    ((real.continuous_abs _ $ is_open_gt' (abs a₁ + 1)).prod
       (real.continuous_abs _ $ is_open_gt' (abs a₂ + 1)))
     ⟨lt_add_one (abs a₁), lt_add_one (abs a₂)⟩)
 

src/topology/local_homeomorph.lean

@@ -496,8 +496,8 @@ section prod
 
 /-- The product of two local homeomorphisms, as a local homeomorphism on the product space. -/
 def prod (e : local_homeomorph α β) (e' : local_homeomorph γ δ) : local_homeomorph (α × γ) (β × δ) :=
-{ open_source := is_open_prod e.open_source e'.open_source,
-  open_target := is_open_prod e.open_target e'.open_target,
+{ open_source := e.open_source.prod e'.open_source,
+  open_target := e.open_target.prod e'.open_target,
   continuous_to_fun := continuous_on.prod
     (e.continuous_to_fun.comp continuous_fst.continuous_on (prod_subset_preimage_fst _ _))
     (e'.continuous_to_fun.comp continuous_snd.continuous_on (prod_subset_preimage_snd _ _)),

src/topology/topological_fiber_bundle.lean

@@ -178,7 +178,7 @@ begin
       simpa [h_source] using h } },
   rw [this, inter_comm],
   exact continuous_on.preimage_open_of_open e.continuous_to_fun e.open_source
-    (is_open_prod u_open is_open_univ)
+    (u_open.prod is_open_univ)
 end
 
 /-- The projection from a topological fiber bundle to its base is continuous. -/
@@ -314,9 +314,9 @@ def triv_change (i j : ι) : local_homeomorph (B × F) (B × F) :=
     { simp [hx] },
   end,
   open_source :=
-    is_open_prod (is_open_inter (Z.is_open_base_set i) (Z.is_open_base_set j)) is_open_univ,
+    (is_open_inter (Z.is_open_base_set i) (Z.is_open_base_set j)).prod is_open_univ,
   open_target :=
-    is_open_prod (is_open_inter (Z.is_open_base_set i) (Z.is_open_base_set j)) is_open_univ,
+    (is_open_inter (Z.is_open_base_set i) (Z.is_open_base_set j)).prod is_open_univ,
   continuous_to_fun  :=
     continuous_on.prod continuous_fst.continuous_on (Z.coord_change_continuous i j),
   continuous_inv_fun := by simpa [inter_comm]
@@ -396,13 +396,13 @@ lemma open_source' (i : ι) : is_open (Z.local_triv' i).source :=
 begin
   apply topological_space.generate_open.basic,
   simp only [exists_prop, mem_Union, mem_singleton_iff],
-  refine ⟨i, set.prod (Z.base_set i) univ, is_open_prod (Z.is_open_base_set i) (is_open_univ), _⟩,
+  refine ⟨i, set.prod (Z.base_set i) univ, (Z.is_open_base_set i).prod is_open_univ, _⟩,
   ext p,
   simp only with mfld_simps
 end
 
 lemma open_target' (i : ι) : is_open (Z.local_triv' i).target :=
-is_open_prod (Z.is_open_base_set i) (is_open_univ)
+(Z.is_open_base_set i).prod is_open_univ
 
 /-- Local trivialization of a topological bundle created from core, as a local homeomorphism. -/
 def local_triv (i : ι) : local_homeomorph Z.total_space (B × F) :=

src/topology/uniform_space/compact_separated.lean

@@ -146,7 +146,7 @@ def uniform_space_of_compact_t2 {α : Type*} [topological_space α] [compact_spa
         { right,
           rw mem_prod,
           tauto }, },
-      all_goals { simp only [is_open_prod, *] } },
+      all_goals { simp only [is_open.prod, *] } },
     -- So W ○ W ∈ F by definition of F
     have : W ○ W ∈ F,
     { dsimp [F],-- Lean has weird elaboration trouble with this line