Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.frontier_set_of_im_lt

Modification history

2022-01-05 14:15

src/analysis/complex/re_im_topology.lean

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

Added complex.frontier_set_of_im_lt View on Github →