Commit 2023-05-16 15:19 0abd4a4f

View on Github →

feat: port Analysis.Complex.ReImTopology (#4013)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/ReImTopology.lean

added theorem Complex.closure_preimage_im

added theorem Complex.closure_preimage_re

added theorem Complex.closure_reProdIm

added theorem Complex.closure_setOf_im_lt

added theorem Complex.closure_setOf_lt_im

added theorem Complex.closure_setOf_lt_re

added theorem Complex.closure_setOf_re_lt

added theorem Complex.frontier_preimage_im

added theorem Complex.frontier_preimage_re

added theorem Complex.frontier_reProdIm

added theorem Complex.frontier_setOf_im_le

added theorem Complex.frontier_setOf_im_lt

added theorem Complex.frontier_setOf_le_im

added theorem Complex.frontier_setOf_le_re

added theorem Complex.frontier_setOf_le_re_and_im_le

added theorem Complex.frontier_setOf_le_re_and_le_im

added theorem Complex.frontier_setOf_lt_im

added theorem Complex.frontier_setOf_lt_re

added theorem Complex.frontier_setOf_re_le

added theorem Complex.frontier_setOf_re_lt

added theorem Complex.interior_preimage_im

added theorem Complex.interior_preimage_re

added theorem Complex.interior_reProdIm

added theorem Complex.interior_setOf_im_le

added theorem Complex.interior_setOf_le_im

added theorem Complex.interior_setOf_le_re

added theorem Complex.interior_setOf_re_le

added theorem Complex.isHomeomorphicTrivialFiberBundle_im

added theorem Complex.isHomeomorphicTrivialFiberBundle_re

added theorem Complex.isOpenMap_im

added theorem Complex.isOpenMap_re

added theorem Complex.quotientMap_im

added theorem Complex.quotientMap_re

added theorem IsClosed.reProdIm

added theorem IsOpen.reProdIm

added theorem Metric.Bounded.reProdIm