Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_open.re_prod_im

Modification history

2022-04-11 11:52
src/analysis/complex/re_im_topology.lean
feat(analysis/complex/re_im_topology): add `metric.bounded.re_prod_im` (#13324) …
Modified is_open.re_prod_imView on Github →
2022-02-09 08:51
src/analysis/complex/re_im_topology.lean
feat(data/complex/basic): re-im set product (#11770) …
Modified is_open.re_prod_imView on Github →
2022-01-17 14:43
src/analysis/complex/re_im_topology.lean
feat(analysis/complex/cauchy_integral): review docs, add versions without `off_countable` (#11417)
Added is_open.re_prod_imView on Github →