Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-11 11:52 d4059557

View on Github →

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

Estimated changes

Modified src/analysis/complex/re_im_topology.lean

modified theorem is_closed.re_prod_im

modified theorem is_open.re_prod_im

added theorem metric.bounded.re_prod_im

Modified src/data/complex/basic.lean

added theorem complex.mem_re_prod_im