Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 14:15 33b5d264

View on Github →

feat(analysis/complex): re, im, and closure/interior/frontier (#11215)

Estimated changes

Modified src/analysis/complex/basic.lean

Created src/analysis/complex/re_im_topology.lean

added theorem complex.closure_preimage_im

added theorem complex.closure_preimage_re

added theorem complex.closure_preimage_re_inter_preimage_im

added theorem complex.closure_set_of_im_lt

added theorem complex.closure_set_of_lt_im

added theorem complex.closure_set_of_lt_re

added theorem complex.closure_set_of_re_lt

added theorem complex.frontier_preimage_im

added theorem complex.frontier_preimage_re

added theorem complex.frontier_preimage_re_inter_preimage_im

added theorem complex.frontier_set_of_im_le

added theorem complex.frontier_set_of_im_lt

added theorem complex.frontier_set_of_le_im

added theorem complex.frontier_set_of_le_re

added theorem complex.frontier_set_of_le_re_and_im_le

added theorem complex.frontier_set_of_le_re_and_le_im

added theorem complex.frontier_set_of_lt_im

added theorem complex.frontier_set_of_lt_re

added theorem complex.frontier_set_of_re_le

added theorem complex.frontier_set_of_re_lt

added theorem complex.interior_preimage_im

added theorem complex.interior_preimage_re

added theorem complex.interior_preimage_re_inter_preimage_im

added theorem complex.interior_set_of_im_le

added theorem complex.interior_set_of_le_im

added theorem complex.interior_set_of_le_re

added theorem complex.interior_set_of_re_le

added theorem complex.is_open_map_im

added theorem complex.is_open_map_re

added theorem complex.is_topological_fiber_bundle_im

added theorem complex.is_topological_fiber_bundle_re

added theorem complex.is_trivial_topological_fiber_bundle_im

added theorem complex.is_trivial_topological_fiber_bundle_re

added theorem complex.quotient_map_im

added theorem complex.quotient_map_re

Modified src/data/complex/basic.lean

modified def complex.equiv_real_prod

deleted theorem complex.equiv_real_prod_apply

deleted theorem complex.equiv_real_prod_symm_im

deleted theorem complex.equiv_real_prod_symm_re

Modified src/topology/homeomorph.lean

added theorem homeomorph.preimage_frontier