feat(analysis/complex/re_im_topology): add metric.bounded.re_prod_im (#13324)

Also add `complex.mem_re_prod_im`.

Author: urkud

src/analysis/complex/re_im_topology.lean

@@ -147,11 +147,15 @@ by simpa only [closure_Ici, closure_Iic, frontier_Ici, frontier_Iic]
 
 end complex
 
-open complex
+open complex metric
 
-lemma is_open.re_prod_im {s t : set ℝ} (hs : is_open s) (ht : is_open t) : is_open (s ×ℂ t) :=
+variables {s t : set ℝ}
+
+lemma is_open.re_prod_im (hs : is_open s) (ht : is_open t) : is_open (s ×ℂ t) :=
 (hs.preimage continuous_re).inter (ht.preimage continuous_im)
 
-lemma is_closed.re_prod_im {s t : set ℝ} (hs : is_closed s) (ht : is_closed t) :
-  is_closed (s ×ℂ t) :=
+lemma is_closed.re_prod_im (hs : is_closed s) (ht : is_closed t) : is_closed (s ×ℂ t) :=
 (hs.preimage continuous_re).inter (ht.preimage continuous_im)
+
+lemma metric.bounded.re_prod_im (hs : bounded s) (ht : bounded t) : bounded (s ×ℂ t) :=
+equiv_real_prodₗ.antilipschitz.bounded_preimage (hs.prod ht)

src/data/complex/basic.lean

@@ -69,6 +69,8 @@ def _root_.set.re_prod_im (s t : set ℝ) : set ℂ := re ⁻¹' s ∩ im ⁻¹'
 
 infix ` ×ℂ `:72 := set.re_prod_im
 
+lemma mem_re_prod_im {z : ℂ} {s t : set ℝ} : z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t := iff.rfl
+
 instance : has_zero ℂ := ⟨(0 : ℝ)⟩
 instance : inhabited ℂ := ⟨0⟩