Commit 2022-02-09 08:51 4e17e081

View on Github →

feat(data/complex/basic): re-im set product (#11770) set.re_im_prod s t (notation: s ×ℂ t) is the product of a set on the real axis and a set on the imaginary axis of the complex plane.

Estimated changes

Modified src/analysis/complex/cauchy_integral.lean

Modified src/analysis/complex/re_im_topology.lean

deleted theorem complex.closure_preimage_re_inter_preimage_im

added theorem complex.closure_re_prod_im

deleted theorem complex.frontier_preimage_re_inter_preimage_im

added theorem complex.frontier_re_prod_im

deleted theorem complex.interior_preimage_re_inter_preimage_im

added theorem complex.interior_re_prod_im

modified theorem is_open.re_prod_im

Modified src/data/complex/basic.lean

added def set.re_prod_im